--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/times.ma".
+
+include "logic/equality.ma".
+include "nat/nat.ma".
+include "nat/plus.ma".
+
+let rec times n m \def
+ match n with
+ [ O \Rightarrow O
+ | (S p) \Rightarrow (plus m (times p m)) ].
+
+theorem times_n_O: \forall n:nat. eq 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)).
+intros.elim n.
+simplify.reflexivity.
+simplify.apply eq_f.rewrite < H.
+transitivity (plus (plus e1 m) (times e1 m)).symmetry.apply assoc_plus.
+transitivity (plus (plus m e1) (times e1 m)).
+apply eq_f2.
+apply sym_plus.
+reflexivity.
+apply assoc_plus.
+qed.
+
+(* same problem with symmetric: see plus
+theorem symmetric_times : symmetric nat times. *)
+
+theorem sym_times :
+\forall n,m:nat. eq nat (times n m) (times m n).
+intros.elim n.
+simplify.apply times_n_O.
+simplify.rewrite > H.apply times_n_Sm.
+qed.
+
+theorem times_plus_distr: \forall n,m,p:nat.
+eq nat (times n (plus m p)) (plus (times n m) (times n p)).
+intros.elim n.
+simplify.reflexivity.
+simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
+apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? p.
+rewrite > assoc_plus.reflexivity.
+qed.