proposition: Lemma zero_or_succ : forall n : nat, n = 0 \/ n = S (pred n).
proof: Proof. Admitted. Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0. Proof. Admitted. Theorem or_commut : forall P Q : Prop, P \/ Q -> Q \/ P. Proof. Admitted. Module NotPlayground. Definition not (P:Prop) := P -> False. Notation "~ x" := (not x) : type_scope. Check not : Prop -> Prop. End NotPlayground. Theorem ex_falso_quodlibet : forall (P:Prop), False -> P. Proof. Admitted. Theorem zero_not_one : 0 <> 1. Proof. unfold not. intros contra. discriminate contra. Qed.