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