proposition: Theorem and_assoc : forall P Q R : Prop, P /\ (Q /\ R) -> (P /\ Q) /\ R.
proof: Proof. intros P Q R [HP [HQ HR]]. Admitted. Check and : Prop -> Prop -> Prop. Lemma factor_is_O: forall n m : nat, n = 0 \/ m = 0 -> n * m = 0. Proof. intros n m [Hn | Hm]. - rewrite Hn. reflexivity. - rewrite Hm. rewrite <- mult_n_O. reflexivity. Qed.