Math
Rules of Inference with Coq
This is a list of proofs with Coq, for each rule of inference stated in List of Rules of Inference (Wikipedia) Some rules that need the law of excluded middle are at the end of the section. Rules for Negation Lemma reductio_ad_absurdum : forall P Q : Prop, (P -&