proposition: Theorem add_comm : ∀ n m, n + m = m + n.
proof: Proof. intros n m. destruct n; [ simpl | destruct m; reflexivity ]. destruct m as [m| ]; [ simpl | reflexivity ]. f_equal. unfold Qplus; simpl. f_equal. rewrite Z.add_comm; reflexivity. rewrite Pos.mul_comm; reflexivity. Qed.
imports: Utf8 QArith Misc