proposition: Theorem iff_refl : forall P : Prop, P <-> P.
proof: Proof. Admitted. Theorem iff_trans : forall P Q R : Prop, (P <-> Q) -> (Q <-> R) -> (P <-> R). Proof. Admitted. Theorem or_distributes_over_and : forall P Q R : Prop, P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R). Proof. Admitted. From Coq Require Import Setoids.Setoid. Lemma mul_eq_0 : forall n m, n * m = 0 <-> n = 0 \/ m = 0. Proof. split. - apply mult_is_O. - apply factor_is_O. Qed.