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