proposition: Lemma or_elim_example : A \/ B -> C.
proof: Proof. move=> aob. case: aob. Abort. Print ex. Lemma ex_elim P : (exists x : A, P x) -> True. Proof. case => x px. Abort. End Connectives. About nat_ind. Definition ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P n.+1) -> forall n : nat, P n := fun P p0 pS => fix IH n : P n := match n with | O => p0 | S p => pS p (IH p) end. Print False. Print True. Check (match 3 with O => I | S _ => I end) : True. Lemma helper x : S x = 0 -> False. Proof. by []. Qed.
imports: mathcomp(all_ssreflect)