[ O \Rightarrow O
| (S p) \Rightarrow (plus m (times p m)) ].
-theorem times_n_O: \forall n:nat. eq nat O (times n O).
+theorem times_n_O: \forall n:nat. O = times n O.
intros.elim n.
simplify.reflexivity.
simplify.assumption.
qed.
theorem times_n_Sm :
-\forall n,m:nat. eq nat (plus n (times n m)) (times n (S m)).
+\forall n,m:nat.plus n (times n m) = times n (S m).
intros.elim n.
simplify.reflexivity.
simplify.apply eq_f.rewrite < H.
theorem symmetric_times : symmetric nat times. *)
theorem sym_times :
-\forall n,m:nat. eq nat (times n m) (times m n).
+\forall n,m:nat.times n m = times m n.
intros.elim n.
simplify.apply times_n_O.
simplify.rewrite > H.apply times_n_Sm.
qed.
variant times_plus_distr: \forall n,m,p:nat.
-eq nat (times n (plus m p)) (plus (times n m) (times n p))
+times n (plus m p) = plus (times n m) (times n p)
\def distributive_times_plus.