(* Things we proved for talk 1. *) Lemma a_nat : nat. Proof. exact (5000). Qed. (* Alternative Proof *) Lemma a_nat': nat. Proof. exact (0). Qed. Print a_nat. Print a_nat'. (* That was an example of proof-irrelevance. The structure of the proof is irrelevant so long as it has the correct type. *) Goal 2 <= 2. Proof. exact (le_n _). Qed. Lemma two_le_four: 2 <= 4. Proof. exact (le_S 2 3 (le_S 2 2 (le_n 2))). Qed. (* Alternate Proof *) Lemma two_le_four' : 2 <= 4. Proof. exact (le_S _ _ (le_S _ _ (le_n _))). Qed. (* The above was not an example of proof irrelevance. The two proofs are identical, it's just that in the second proof we allowed the Coq engine to infer values at the location of the underscores. *)