proposition: Theorem eq_add_0 : ∀ n m, n + m = 0 ↔ n = 0 ∧ m = 0.
proof: Proof. intros n m. destruct n as [n| ]; simpl. destruct m as [m| ]; simpl. split; intros H. injection H; clear H; intros H. apply Nat.eq_add_0 in H. destruct H; subst; split; reflexivity. destruct H as (Hn, Hm). injection Hn; intros; subst. injection Hm; intros; subst; reflexivity. split; intros H; [ discriminate H | destruct H; assumption ]. split; intros H; [ discriminate H | destruct H; assumption ]. Qed.
imports: Utf8 Compare_dec NPeano Misc