1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/times".
17 include "logic/equality.ma".
19 include "nat/plus.ma".
21 let rec times n m \def
24 | (S p) \Rightarrow (plus m (times p m)) ].
26 theorem times_n_O: \forall n:nat. eq nat O (times n O).
33 \forall n,m:nat. eq nat (plus n (times n m)) (times n (S m)).
36 simplify.apply eq_f.rewrite < H.
37 transitivity (plus (plus e1 m) (times e1 m)).symmetry.apply assoc_plus.
38 transitivity (plus (plus m e1) (times e1 m)).
45 (* same problem with symmetric: see plus
46 theorem symmetric_times : symmetric nat times. *)
49 \forall n,m:nat. eq nat (times n m) (times m n).
51 simplify.apply times_n_O.
52 simplify.rewrite > H.apply times_n_Sm.
55 theorem times_plus_distr: \forall n,m,p:nat.
56 eq nat (times n (plus m p)) (plus (times n m) (times n p)).
59 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
60 apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? p.
61 rewrite > assoc_plus.reflexivity.