proposition: Theorem add_comm : ∀ n m, n + m = m + n.
proof: Proof. intros n m. destruct n; [ simpl | destruct m; reflexivity ]. destruct m; [ rewrite Nat.add_comm; reflexivity | reflexivity ]. Qed.
imports: Utf8 Compare_dec NPeano Misc