From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 12 Oct 2007 09:57:49 +0000 (+0000)
Subject: Reorganization of results.
X-Git-Tag: 0.4.95@7852~140
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c0d9ea5098c4b271fce972b685ea6a1ed4cd671;p=helm.git

Reorganization of results.
---

diff --git a/matita/library/Z/dirichlet_product.ma b/matita/library/Z/dirichlet_product.ma
index edc203761..6328bc7dc 100644
--- a/matita/library/Z/dirichlet_product.ma
+++ b/matita/library/Z/dirichlet_product.ma
@@ -23,417 +23,6 @@ definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def
 sigma_p (S n) 
  (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
 
-(* da spostare *)
-
-(* spostati in div_and_mod.ma
-theorem mod_SO: \forall n:nat. mod n (S O) = O.
-intro.
-apply sym_eq.
-apply le_n_O_to_eq.
-apply le_S_S_to_le.
-apply lt_mod_m_m.
-apply le_n.
-qed.
-theorem div_SO: \forall n:nat. div n (S O) = n.
-intro.
-rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
-  [rewrite > mod_SO.
-   rewrite < plus_n_O.
-   apply times_n_SO
-  |apply le_n
-  ]
-qed.*)
-
-theorem and_true: \forall a,b:bool. 
-andb a b =true \to a =true \land b= true.
-intro.elim a
-  [split
-    [reflexivity|assumption]
-  |apply False_ind.
-   apply not_eq_true_false.
-   apply sym_eq.
-   assumption
-  ]
-qed.
-
-theorem lt_times_plus_times: \forall a,b,n,m:nat. 
-a < n \to b < m \to a*m + b < n*m.
-intros 3.
-apply (nat_case n)
-  [intros.apply False_ind.apply (not_le_Sn_O ? H)
-  |intros.simplify.
-   rewrite < sym_plus.
-   unfold.
-   change with (S b+a*m1 \leq m1+m*m1).
-   apply le_plus
-    [assumption
-    |apply le_times
-      [apply le_S_S_to_le.assumption
-      |apply le_n
-      ]
-    ]
-  ]
-qed.
-
-theorem divides_to_divides_b_true1 : \forall n,m:nat.
-O < m \to n \divides m \to divides_b n m = true.
-intro.
-elim (le_to_or_lt_eq O n (le_O_n n))
-  [apply divides_to_divides_b_true
-    [assumption|assumption]
-  |apply False_ind.
-   rewrite < H in H2.
-   elim H2.
-   simplify in H3.
-   apply (not_le_Sn_O O).
-   rewrite > H3 in H1.
-   assumption
-  ]
-qed.
-(* spostato in primes.ma
-theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
-intro.
-elim (le_to_or_lt_eq O n (le_O_n n))
-  [rewrite > plus_n_O.
-   rewrite < (divides_to_mod_O ? ? H H1).
-   apply sym_eq.
-   apply div_mod.
-   assumption
-  |elim H1.
-   generalize in match H2.
-   rewrite < H.
-   simplify.
-   intro.
-   rewrite > H3.
-   reflexivity
-  ]
-qed.*)
-(* spostato in div_and_mod.ma
-theorem le_div: \forall n,m. O < n \to m/n \le m.
-intros.
-rewrite > (div_mod m n) in \vdash (? ? %)
-  [apply (trans_le ? (m/n*n))
-    [rewrite > times_n_SO in \vdash (? % ?).
-     apply le_times
-      [apply le_n|assumption]
-    |apply le_plus_n_r
-    ]
-  |assumption
-  ]
-qed.*)
-  
-theorem sigma_p2_eq: 
-\forall g: nat \to nat \to Z.
-\forall h11,h12,h21,h22: nat \to nat \to nat. 
-\forall n,m.
-\forall p11,p21:nat \to bool.
-\forall p12,p22:nat \to nat \to bool.
-(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
-p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
-\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
-\land h11 i j < n \land h12 i j < m) \to
-(\forall i,j. i < n \to j < m \to p11 i = true \to p12 i j = true \to 
-p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
-\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
-\land (h21 i j) < n \land (h22 i j) < m) \to
-sigma_p n p11 (\lambda x:nat .sigma_p m (p12 x) (\lambda y. g x y)) =
-sigma_p n p21 (\lambda x:nat .sigma_p m (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
-intros.
-rewrite < sigma_p2'.
-rewrite < sigma_p2'.
-apply sym_eq.
-letin h := (\lambda x.(h11 (x/m) (x\mod m))*m + (h12 (x/m) (x\mod m))).
-letin h1 := (\lambda x.(h21 (x/m) (x\mod m))*m + (h22 (x/m) (x\mod m))).
-apply (trans_eq ? ? 
-  (sigma_p (n*m) (\lambda x:nat.p21 (x/m)\land p22 (x/m) (x\mod m))
-  (\lambda x:nat.g ((h x)/m) ((h x)\mod m))))
-  [clear h.clear h1.
-   apply eq_sigma_p1
-    [intros.reflexivity
-    |intros.
-     cut (O < m)
-      [cut (x/m < n)
-        [cut (x \mod m < m)
-          [elim (and_true ? ? H3).
-           elim (H ? ? Hcut1 Hcut2 H4 H5).
-           elim H6.clear H6.
-           elim H8.clear H8.
-           elim H6.clear H6.
-           elim H8.clear H8.
-           apply eq_f2
-            [apply sym_eq.
-             apply div_plus_times.
-             assumption
-            |autobatch
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m)
-          [assumption
-          |apply (le_to_lt_to_lt ? x)
-            [apply (eq_plus_to_le ? ? (x \mod m)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H2.
-       apply (le_n_O_elim ? H4).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]      
-    ]
-  |apply (eq_sigma_p_gh ? h h1);intros
-    [cut (O < m)
-      [cut (i/m < n)
-        [cut (i \mod m < m)
-          [elim (and_true ? ? H3).
-           elim (H ? ? Hcut1 Hcut2 H4 H5).
-           elim H6.clear H6.
-           elim H8.clear H8.
-           elim H6.clear H6.
-           elim H8.clear H8.
-           cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m = 
-                 h11 (i/m) (i\mod m))
-            [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
-                  h12 (i/m) (i\mod m))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.
-               rewrite > H6.
-               rewrite > H12.
-               reflexivity
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m)
-          [assumption
-          |apply (le_to_lt_to_lt ? i)
-            [apply (eq_plus_to_le ? ? (i \mod m)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H2.
-       apply (le_n_O_elim ? H4).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]      
-    |cut (O < m)
-      [cut (i/m < n)
-        [cut (i \mod m < m)
-          [elim (and_true ? ? H3).
-           elim (H ? ? Hcut1 Hcut2 H4 H5).
-           elim H6.clear H6.
-           elim H8.clear H8.
-           elim H6.clear H6.
-           elim H8.clear H8.
-           cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m = 
-                 h11 (i/m) (i\mod m))
-            [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
-                  h12 (i/m) (i\mod m))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.
-               rewrite > H10.
-               rewrite > H11.
-               apply sym_eq.
-               apply div_mod.
-               assumption
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m)
-          [assumption
-          |apply (le_to_lt_to_lt ? i)
-            [apply (eq_plus_to_le ? ? (i \mod m)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H2.
-       apply (le_n_O_elim ? H4).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]      
-    |cut (O < m)
-      [cut (i/m < n)
-        [cut (i \mod m < m)
-          [elim (and_true ? ? H3).
-           elim (H ? ? Hcut1 Hcut2 H4 H5).
-           elim H6.clear H6.
-           elim H8.clear H8.
-           elim H6.clear H6.
-           elim H8.clear H8.
-           apply lt_times_plus_times
-            [assumption|assumption]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m)
-          [assumption
-          |apply (le_to_lt_to_lt ? i)
-            [apply (eq_plus_to_le ? ? (i \mod m)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H2.
-       apply (le_n_O_elim ? H4).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]
-    |cut (O < m)
-      [cut (j/m < n)
-        [cut (j \mod m < m)
-          [elim (and_true ? ? H3).
-           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
-           elim H6.clear H6.
-           elim H8.clear H8.
-           elim H6.clear H6.
-           elim H8.clear H8.
-           cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m = 
-                 h21 (j/m) (j\mod m))
-            [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
-                  h22 (j/m) (j\mod m))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.
-               rewrite > H6.
-               rewrite > H12.
-               reflexivity
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ] 
-        |apply (lt_times_n_to_lt m)
-          [assumption
-          |apply (le_to_lt_to_lt ? j)
-            [apply (eq_plus_to_le ? ? (j \mod m)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H2.
-       apply (le_n_O_elim ? H4).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ] 
-    |cut (O < m)
-      [cut (j/m < n)
-        [cut (j \mod m < m)
-          [elim (and_true ? ? H3).
-           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
-           elim H6.clear H6.
-           elim H8.clear H8.
-           elim H6.clear H6.
-           elim H8.clear H8.
-           cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m = 
-                 h21 (j/m) (j\mod m))
-            [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
-                  h22 (j/m) (j\mod m))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.               
-               rewrite > H10.
-               rewrite > H11.
-               apply sym_eq.
-               apply div_mod.
-               assumption
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ] 
-        |apply (lt_times_n_to_lt m)
-          [assumption
-          |apply (le_to_lt_to_lt ? j)
-            [apply (eq_plus_to_le ? ? (j \mod m)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H2.
-       apply (le_n_O_elim ? H4).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ] 
-    |cut (O < m)
-      [cut (j/m < n)
-        [cut (j \mod m < m)
-          [elim (and_true ? ? H3).
-           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
-           elim H6.clear H6.
-           elim H8.clear H8.
-           elim H6.clear H6.
-           elim H8.clear H8.
-           apply (lt_times_plus_times ? ? ? m)
-            [assumption|assumption]
-          |apply lt_mod_m_m.
-           assumption
-          ] 
-        |apply (lt_times_n_to_lt m)
-          [assumption
-          |apply (le_to_lt_to_lt ? j)
-            [apply (eq_plus_to_le ? ? (j \mod m)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H2.
-       apply (le_n_O_elim ? H4).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]
-    ]
-  ]
-qed.
-     
 (* dirichlet_product is associative only up to extensional equality *)
 theorem associative_dirichlet_product: 
 \forall f,g,h:nat\to Z.\forall n:nat.O < n \to
@@ -488,6 +77,8 @@ apply (trans_eq ? ?
         (\lambda d,d1:nat.d/d1)
         (S n)
         (S n)
+        (S n)
+        (S n)
         ?
         ?
         (\lambda d,d1:nat.divides_b d1 d)
@@ -773,44 +364,6 @@ intro.apply (nat_case n)
   ]
 qed.
 
-(* da spostare in times *)
-definition Zone \def pos O.
-
-theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
-intro.unfold Zone.simplify.
-elim z;simplify
-  [reflexivity
-  |rewrite < plus_n_O.reflexivity
-  |rewrite < plus_n_O.reflexivity
-  ]
-qed.
-
-theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
-intro.
-rewrite < sym_Ztimes.
-apply Ztimes_Zone_l.
-qed.
-
-theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
-intro.simplify.intros (z y).
-rewrite < Zplus_z_OZ.
-rewrite < (Zplus_z_OZ y).
-rewrite < (Zplus_Zopp x).
-rewrite < (Zplus_Zopp x).
-rewrite < assoc_Zplus.
-rewrite < assoc_Zplus.
-apply eq_f2
-  [assumption|reflexivity]
-qed.
-
-theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
-intro.simplify.intros (z y).
-apply (injective_Zplus_l x).
-rewrite < sym_Zplus.
-rewrite > H.
-apply sym_Zplus.
-qed.
-
 theorem sigma_p_OZ:
 \forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
 intros.elim n
@@ -887,64 +440,6 @@ elim n
   ]
 qed.           
 
-(* da spostare *)
-theorem notb_notb: \forall b:bool. notb (notb b) = b.
-intros.
-elim b;reflexivity.
-qed.
-
-theorem injective_notb: injective bool bool notb.
-unfold injective.
-intros.
-rewrite < notb_notb.
-rewrite < (notb_notb y).
-apply eq_f.
-assumption.
-qed.
-
-theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
-intros.
-apply (witness ? ? d).
-apply sym_eq.
-apply divides_to_div.
-assumption.
-qed.
-
-theorem divides_b_div_true: 
-\forall d,n. O < n \to 
-  divides_b d n = true \to divides_b (n/d) n = true.
-intros.
-apply divides_to_divides_b_true1
-  [assumption
-  |apply divides_div.
-   apply divides_b_true_to_divides.
-   assumption
-  ]
-qed.
-
-(* spostato in primes.ma (non in div_and_mod.ma perche' serve il predicato divides)
-theorem div_div: \forall n,d:nat. O < n \to divides d n \to 
-n/(n/d) = d.
-intros.
-apply (inj_times_l1 (n/d))
-  [apply (lt_times_n_to_lt d)
-    [apply (divides_to_lt_O ? ? H H1).
-    |rewrite > divides_to_div;assumption
-    ]
-  |rewrite > divides_to_div
-    [rewrite > sym_times.
-     rewrite > divides_to_div
-      [reflexivity
-      |assumption
-      ]
-    |apply (witness ? ? d).
-     apply sym_eq.
-     apply divides_to_div.
-     assumption
-    ]
-  ]
-qed.
-*)
 theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to 
 dirichlet_product f g n = dirichlet_product g f n.
 intros.
diff --git a/matita/library/Z/moebius.ma b/matita/library/Z/moebius.ma
index 33c9ad4be..d2c3765c3 100644
--- a/matita/library/Z/moebius.ma
+++ b/matita/library/Z/moebius.ma
@@ -40,6 +40,7 @@ definition moebius : nat \to Z \def
   let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
   moebius_aux (S p) n.
 
+(*
 theorem moebius_O : moebius O = pos O.
 simplify. reflexivity.
 qed.
@@ -56,6 +57,10 @@ theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
 simplify.reflexivity.
 qed.
 
+theorem moebius_SSSSO : moebius (S (S (S (S O)))) = OZ.
+simplify.reflexivity.
+qed.
+*)
 
 theorem not_divides_to_p_ord_O: \forall n,i.
 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = 
diff --git a/matita/library/Z/orders.ma b/matita/library/Z/orders.ma
index 0a3cfbe1f..06b6a1ec4 100644
--- a/matita/library/Z/orders.ma
+++ b/matita/library/Z/orders.ma
@@ -76,6 +76,121 @@ cut (pos n < pos n \to False).
 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 qed.
 
+(* transitivity *)
+theorem transitive_Zle : transitive Z Zle.
+unfold transitive.
+intros 3.
+elim x 0
+[ (* x = OZ *)
+  elim y 0
+  [ intros. assumption 
+  | intro.
+    elim z
+    [ simplify. apply I 
+    | simplify. apply I
+    | simplify. simplify in H1. assumption
+    ]
+  | intro.
+    elim z
+    [ simplify. apply I
+    | simplify. apply I
+    | simplify. simplify in H. assumption
+    ]
+  ]
+| (* x = (pos n) *)
+  intro.
+  elim y 0
+  [ intros. apply False_ind. apply H
+  | intros 2. 
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. generalize in match H. simplify. apply trans_le 
+    | intro. simplify. intro. assumption
+    ]
+  | intros 2. apply False_ind. apply H
+  ]
+| (* x = (neg n) *)
+  intro.
+  elim y 0
+  [ elim z 0
+    [ simplify. intros. assumption
+    | intro. simplify. intros. assumption
+    | intro. simplify. intros. apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z
+    [ apply False_ind. apply H1 
+    | simplify. apply I
+    | apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. simplify. intro. assumption
+    | intros. simplify. simplify in H. simplify in H1. 
+      generalize in match H. generalize in match H1. apply trans_le
+    ]
+  ]
+]
+qed.
+
+variant trans_Zle: transitive Z Zle
+\def transitive_Zle.
+
+theorem transitive_Zlt: transitive Z Zlt.
+unfold.
+intros 3.
+elim x 0
+[ (* x = OZ *)
+  elim y 0
+  [ intros. apply False_ind. apply H 
+  | intro.
+    elim z
+    [ simplify. apply H1 
+    | simplify. apply I
+    | simplify. apply H1
+    ]
+  | intros 2. apply False_ind. apply H
+  ]
+| (* x = (pos n) *)
+  intro.
+  elim y 0
+  [ intros. apply False_ind. apply H
+  | intros 2. 
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. generalize in match H. simplify. apply trans_lt 
+    | intro. simplify. intro. assumption
+    ]
+  | intros 2. apply False_ind. apply H
+  ]
+| (* x = (neg n) *)
+  intro.
+  elim y 0
+  [ elim z 0
+    [ intros. simplify. apply I
+    | intro. simplify. intros. assumption
+    | intro. simplify. intros. apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z
+    [ apply False_ind. apply H1 
+    | simplify. apply I
+    | apply False_ind. apply H1
+    ]
+  | intros 2.
+    elim z 0
+    [ simplify. intro. assumption
+    | intro. simplify. intro. assumption
+    | intros. simplify. simplify in H. simplify in H1. 
+      generalize in match H. generalize in match H1. apply trans_lt
+    ]
+  ]
+]
+qed.
+
+variant trans_Zlt: transitive Z Zlt
+\def transitive_Zlt.
 theorem irrefl_Zlt: irreflexive Z Zlt
 \def irreflexive_Zlt.
 
diff --git a/matita/library/Z/plus.ma b/matita/library/Z/plus.ma
index 2b439b92e..cd5651245 100644
--- a/matita/library/Z/plus.ma
+++ b/matita/library/Z/plus.ma
@@ -261,6 +261,10 @@ definition Zopp : Z \to Z \def
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/plus/Zopp.con x).
 
+theorem eq_OZ_Zopp_OZ : OZ = (- OZ).
+reflexivity.
+qed.
+
 theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
 intros.
 elim x.elim y.
@@ -299,6 +303,26 @@ rewrite > nat_compare_n_n.
 simplify.apply refl_eq.
 qed.
 
+theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
+intro.simplify.intros (z y).
+rewrite < Zplus_z_OZ.
+rewrite < (Zplus_z_OZ y).
+rewrite < (Zplus_Zopp x).
+rewrite < (Zplus_Zopp x).
+rewrite < assoc_Zplus.
+rewrite < assoc_Zplus.
+apply eq_f2
+  [assumption|reflexivity]
+qed.
+
+theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
+intro.simplify.intros (z y).
+apply (injective_Zplus_l x).
+rewrite < sym_Zplus.
+rewrite > H.
+apply sym_Zplus.
+qed.
+
 (* minus *)
 definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
 
diff --git a/matita/library/Z/sigma_p.ma b/matita/library/Z/sigma_p.ma
index b246b8444..8b4c87d3e 100644
--- a/matita/library/Z/sigma_p.ma
+++ b/matita/library/Z/sigma_p.ma
@@ -312,3 +312,317 @@ apply eq_sigma_p
   |intros.apply sym_Ztimes
   ]
 qed.
+
+
+(* sigma from n1*m1 to n2*m2 *)
+theorem sigma_p2_eq: 
+\forall g: nat \to nat \to Z.
+\forall h11,h12,h21,h22: nat \to nat \to nat. 
+\forall n1,m1,n2,m2.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n1 \land h12 i j < m1) \to
+(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n2 \land (h22 i j) < m2) \to
+sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
+sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
+intros.
+rewrite < sigma_p2'.
+rewrite < sigma_p2'.
+apply sym_eq.
+letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
+letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
+apply (trans_eq ? ? 
+  (sigma_p (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2))
+  (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1))))
+  [clear h.clear h1.
+   apply eq_sigma_p1
+    [intros.reflexivity
+    |intros.
+     cut (O < m2)
+      [cut (x/m2 < n2)
+        [cut (x \mod m2 < m2)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           apply eq_f2
+            [apply sym_eq.
+             apply div_plus_times.
+             assumption
+            |autobatch
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m2)
+          [assumption
+          |apply (le_to_lt_to_lt ? x)
+            [apply (eq_plus_to_le ? ? (x \mod m2)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]      
+    ]
+  |apply (eq_sigma_p_gh ? h h1);intros
+    [cut (O < m2)
+      [cut (i/m2 < n2)
+        [cut (i \mod m2 < m2)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
+                 h11 (i/m2) (i\mod m2))
+            [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
+                  h12 (i/m2) (i\mod m2))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.
+               rewrite > H6.
+               rewrite > H12.
+               reflexivity
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m2)
+          [assumption
+          |apply (le_to_lt_to_lt ? i)
+            [apply (eq_plus_to_le ? ? (i \mod m2)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]      
+    |cut (O < m2)
+      [cut (i/m2 < n2)
+        [cut (i \mod m2 < m2)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
+                 h11 (i/m2) (i\mod m2))
+            [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
+                  h12 (i/m2) (i\mod m2))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.
+               rewrite > H10.
+               rewrite > H11.
+               apply sym_eq.
+               apply div_mod.
+               assumption
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m2)
+          [assumption
+          |apply (le_to_lt_to_lt ? i)
+            [apply (eq_plus_to_le ? ? (i \mod m2)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]      
+    |cut (O < m2)
+      [cut (i/m2 < n2)
+        [cut (i \mod m2 < m2)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           apply lt_times_plus_times
+            [assumption|assumption]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m2)
+          [assumption
+          |apply (le_to_lt_to_lt ? i)
+            [apply (eq_plus_to_le ? ? (i \mod m2)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]
+    |cut (O < m1)
+      [cut (j/m1 < n1)
+        [cut (j \mod m1 < m1)
+          [elim (and_true ? ? H3).
+           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
+                 h21 (j/m1) (j\mod m1))
+            [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
+                  h22 (j/m1) (j\mod m1))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.
+               rewrite > H6.
+               rewrite > H12.
+               reflexivity
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ] 
+        |apply (lt_times_n_to_lt m1)
+          [assumption
+          |apply (le_to_lt_to_lt ? j)
+            [apply (eq_plus_to_le ? ? (j \mod m1)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ] 
+    |cut (O < m1)
+      [cut (j/m1 < n1)
+        [cut (j \mod m1 < m1)
+          [elim (and_true ? ? H3).
+           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
+                 h21 (j/m1) (j\mod m1))
+            [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
+                  h22 (j/m1) (j\mod m1))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.               
+               rewrite > H10.
+               rewrite > H11.
+               apply sym_eq.
+               apply div_mod.
+               assumption
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ] 
+        |apply (lt_times_n_to_lt m1)
+          [assumption
+          |apply (le_to_lt_to_lt ? j)
+            [apply (eq_plus_to_le ? ? (j \mod m1)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ] 
+    |cut (O < m1)
+      [cut (j/m1 < n1)
+        [cut (j \mod m1 < m1)
+          [elim (and_true ? ? H3).
+           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           apply (lt_times_plus_times ? ? ? m2)
+            [assumption|assumption]
+          |apply lt_mod_m_m.
+           assumption
+          ] 
+        |apply (lt_times_n_to_lt m1)
+          [assumption
+          |apply (le_to_lt_to_lt ? j)
+            [apply (eq_plus_to_le ? ? (j \mod m1)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]
+    ]
+  ]
+qed.
\ No newline at end of file
diff --git a/matita/library/Z/times.ma b/matita/library/Z/times.ma
index 58de9c827..90a71b520 100644
--- a/matita/library/Z/times.ma
+++ b/matita/library/Z/times.ma
@@ -42,6 +42,8 @@ simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
+definition Zone \def pos O.
+
 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
 neg n * x = - (pos n * x).
 intros.elim x.
@@ -68,6 +70,21 @@ qed.
 variant sym_Ztimes : \forall x,y:Z. x*y = y*x
 \def symmetric_Ztimes.
 
+theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
+intro.unfold Zone.simplify.
+elim z;simplify
+  [reflexivity
+  |rewrite < plus_n_O.reflexivity
+  |rewrite < plus_n_O.reflexivity
+  ]
+qed.
+
+theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
+intro.
+rewrite < sym_Ztimes.
+apply Ztimes_Zone_l.
+qed.
+
 theorem associative_Ztimes: associative Z Ztimes.
 unfold associative.
 intros.elim x.
diff --git a/matita/library/Z/z.ma b/matita/library/Z/z.ma
index d8b829ec1..64b608cb9 100644
--- a/matita/library/Z/z.ma
+++ b/matita/library/Z/z.ma
@@ -34,6 +34,11 @@ definition neg_Z_of_nat \def
 [ O \Rightarrow  OZ 
 | (S n)\Rightarrow  neg n].
 
+lemma pos_n_eq_S_n : \forall n : nat.
+  (pos n) = (S n).
+intro.reflexivity. 
+qed.
+
 definition abs \def
 \lambda z.
  match z with