proposition: Lemma and_example3 : forall n m : nat, n + m = 0 -> n * m = 0.
proof: Proof. intros n m H. assert (H' : n = 0 /\ m = 0). { apply and_exercise. apply H. } destruct H' as [Hn Hm]. rewrite Hn. reflexivity. Qed.
imports: Tactics