proposition: Lemma and_example3 : forall n m : nat, n + m = 0 -> n * m = 0.
proof: Proof. 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.