proposition: Lemma example_spec2 a b : (a <= b) || (b < a).
proof: Proof. case: leqP. Abort. About ltngtP. Print compare_nat. Lemma example_spec3 a b : (a <= b) || (b < a) || (b == a). Proof. case: ltngtP. Abort. About prime_gt1. Lemma example_2 x y : prime x -> odd y -> 2 < y + x. Proof. move/prime_gt1 => x_gt_1. Undo. move/prime_gt1/ltnW. Abort. Lemma example_3 A B (V: A <-> B): B -> A . Proof. move=>b. apply/V. by []. Qed.
imports: mathcomp(all_ssreflect)