proposition: Lemma and_example2 : forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
proof: Proof. Admitted. Lemma and_example2' : forall n m : nat, n = 0 /\ m = 0 -> n + m = 0. Proof. intros n m [Hn Hm]. rewrite Hn. rewrite Hm. reflexivity. Qed.