X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=683ec262773cbe38541ba1499b6cf1eeb3775440;hb=68dbcd02022874a025a9444aa1125b0458816fbb;hp=cce6626a0f43d9273c23a2be0ea6fa90fd55a105;hpb=6d49a181a1b771f797d37b02661b5743aee86ac1;p=helm.git

diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma
index cce6626a0..683ec2627 100644
--- a/helm/software/matita/library/nat/lt_arith.ma
+++ b/helm/software/matita/library/nat/lt_arith.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/lt_arith".
-
 include "nat/div_and_mod.ma".
 
 (* plus *)
@@ -118,6 +116,17 @@ apply (nat_case1 a)
 ]
 qed.
 
+lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
+intros.
+elim (le_to_or_lt_eq O ? (le_O_n m))
+  [assumption
+  |apply False_ind.
+   rewrite < H1 in H.
+   rewrite < times_n_O in H.
+   apply (not_le_Sn_O ? H)
+  ]
+qed.
+
 (* times *)
 theorem monotonic_lt_times_r: 
 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
@@ -239,6 +248,8 @@ apply (nat_case n)
   ]
 qed.
 
+
+
 theorem nat_compare_times_l : \forall n,p,q:nat. 
 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 intros.apply nat_compare_elim.intro.
@@ -262,6 +273,26 @@ apply lt_to_not_eq.assumption.
 intro.reflexivity.
 qed.
 
+(* times and plus *)
+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.
+
 (* div *) 
 
 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m. 
@@ -300,7 +331,81 @@ apply (trans_lt ? (S O)).
 unfold lt. apply le_n.assumption.
 qed.
 
+theorem eq_div_div_div_times: \forall n,m,q. O < n \to O < m \to
+q/n/m = q/(n*m).
+intros.
+apply (div_mod_spec_to_eq q (n*m) ? (q\mod n+n*(q/n\mod m)) ? (mod q (n*m)))
+  [apply div_mod_spec_intro
+    [apply (lt_to_le_to_lt ? (n*(S (q/n\mod m))))
+      [rewrite < times_n_Sm.
+       apply lt_plus_l.
+       apply lt_mod_m_m.
+       assumption
+      |apply le_times_r.
+       apply lt_mod_m_m.
+       assumption
+      ]
+    |rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
+     rewrite < assoc_times.
+     rewrite > (eq_times_div_minus_mod ? ? H1).
+     rewrite > sym_times.
+     rewrite > distributive_times_minus.
+     rewrite > sym_times.
+     rewrite > (eq_times_div_minus_mod ? ? H).
+     rewrite < sym_plus in ⊢ (? ? ? (? ? %)).
+     rewrite < assoc_plus.
+     rewrite < plus_minus_m_m
+      [rewrite < plus_minus_m_m
+        [reflexivity
+        |apply (eq_plus_to_le ? ? ((q/n)*n)).
+         rewrite < sym_plus.
+         apply div_mod.
+         assumption
+        ]
+      |apply (trans_le ? (n*(q/n)))
+        [apply le_times_r.
+         apply (eq_plus_to_le ? ? ((q/n)/m*m)).
+         rewrite < sym_plus.
+         apply div_mod.
+         assumption
+        |rewrite > sym_times.
+         rewrite > eq_times_div_minus_mod
+          [apply le_n
+          |assumption
+          ]
+        ]
+      ]
+    ]
+  |apply div_mod_spec_div_mod.
+   rewrite > (times_n_O O).
+   apply lt_times;assumption
+  ]
+qed.
+
+theorem eq_div_div_div_div: \forall n,m,q. O < n \to O < m \to
+q/n/m = q/m/n.
+intros.
+apply (trans_eq ? ? (q/(n*m)))
+  [apply eq_div_div_div_times;assumption
+  |rewrite > sym_times.
+   apply sym_eq.
+   apply eq_div_div_div_times;assumption
+  ]
+qed.
 
+theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)).
+intros.
+rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
+  [rewrite > eq_div_div_div_div
+    [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
+     apply div_mod.
+     apply lt_O_S
+    |apply lt_O_S
+    |assumption
+    ]
+  |apply lt_O_S
+  ]
+qed.
 (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
 (* The theorem is shown in two different parts: *)