X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fpropr_div_mod_lt_le_totient1_aux.ma;h=9751143068b5790e894772c2264c2d5c688d5702;hb=e65e31bab82994cf8400bb4c294cf7d16fa2c83c;hp=6a5fc2058072bb0bc04f2d858fd9f3fc6259c94c;hpb=a9f72dea3b74e3c0c33daf5be8f4d5d75611492c;p=helm.git

diff --git a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
index 6a5fc2058..975114306 100644
--- a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
+++ b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma
@@ -73,16 +73,11 @@ qed.
 theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat.
 (S O) \lt n \to O \lt (pred n).
 intros.
-elim H
-[ simplify.
-  apply (lt_O_S O)
-| rewrite < (pred_Sn n1).
-  apply (lt_to_le_to_lt O (S (S O)) n1)
-  [ apply le_S.
-    apply (le_n (S O))
-  | assumption
-  ]
-]
+apply (Sa_le_b_to_O_lt_b (pred (S O)) (pred n) ?).
+ apply (lt_pred (S O) n ? ?);
+ [ apply (lt_O_S O) 
+ | apply (H)
+ ]
 qed.
 
 
@@ -91,14 +86,12 @@ O \lt m \to m \divides n \to (n / m) * m = n.
 intros.
 rewrite > plus_n_O.
 apply sym_eq.
-cut (O = n \mod m)
-[ rewrite > Hcut.
+cut (n \mod m = O)
+[ rewrite < Hcut.
   apply div_mod.
   assumption
-| apply sym_eq.
-  apply divides_to_mod_O;
+| apply divides_to_mod_O;
     assumption.
-  
 ]
 qed.
 
@@ -119,77 +112,21 @@ apply (le_times_to_le c (a/c) a)
 qed.
 
 
-theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat.
-O \lt b \to (b*c) \le a \to c \le (a /b).
-intros.
-rewrite > (div_mod a b) in H1
-[ apply (le_times_to_le b ? ?)
-  [ assumption
-  | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b))
-    [ elim Hcut
-      [ rewrite < (sym_times c b).
-        rewrite < (sym_times (a/b) b).
-        assumption
-      | cut (a/b \lt c)
-        [ change in Hcut1 with ((S (a/b)) \le c).
-          cut( b*(S (a/b)) \le b*c)
-          [ rewrite > (sym_times b (S (a/b))) in Hcut2.
-            simplify in Hcut2.
-            cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b)))
-            [ cut (b \le (a \mod b))
-              [ apply False_ind.
-                apply (lt_to_not_le (a \mod b) b)
-                [ apply (lt_mod_m_m).
-                  assumption
-                | assumption
-                ]
-              | apply (le_plus_to_le ((a/b)*b)).
-                rewrite > sym_plus.
-                assumption.
-              ]
-            | apply (trans_le ? (b*c) ?);
-                assumption
-            ]
-          | apply (le_times_r b ? ?).
-            assumption
-          ]
-        | apply (lt_times_n_to_lt b (a/b) c)
-          [ assumption
-          | assumption
-          ]
-        ]
-      ]
-    | apply (leb_elim (c*b) ((a/b)*b))
-      [ intros.
-        left.
-        assumption
-      | intros.
-        right.
-        apply cic:/matita/nat/orders/not_le_to_lt.con. 
-        assumption        
-      ]
-    ]
-  ]
-| assumption
-] 
-qed.
-
 theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb:
 \forall a,b:nat.
 O \lt a \to O \lt b \to a \divides b \to O \lt (b/a).
 intros.
 elim H2.
-cut (O \lt n2)
-[ rewrite > H3.
-  rewrite > (sym_times a n2).
-  rewrite > (div_times_ltO n2 a);
-    assumption  
-| apply (divides_to_lt_O n2 b)
+rewrite > H3.
+rewrite > (sym_times a n2).
+rewrite > (div_times_ltO n2 a)
+[ apply (divides_to_lt_O n2 b)
   [ assumption
   | apply (witness n2 b a).
     rewrite > sym_times.
     assumption
-  ] 
+  ]  
+| assumption  
 ]
 qed.
 
@@ -215,60 +152,30 @@ cut(O \lt c)
 ]
 qed.
 
-
+(*
 theorem div_times_to_eqSO: \forall a,d:nat.
 O \lt d \to a*d = d \to a = (S O).
 intros.
-rewrite > (plus_n_O d) in H1:(? ? ? %).
-cut (a*d -d = O)
-[ rewrite  > sym_times in Hcut.
-  rewrite > times_n_SO in Hcut:(? ? (? ? %) ?).
-  rewrite < distr_times_minus in Hcut.
-  cut ((a - (S O)) = O)
-  [ apply (minus_to_plus a (S O) O)
-    [ apply (nat_case1 a)
-      [ intros.
-        rewrite > H2 in H1.
-        simplify in H1.
-        rewrite < (plus_n_O d) in H1.
-        rewrite < H1 in H.
-        apply False_ind.
-        change in H with ((S O) \le O).
-        apply (not_le_Sn_O O H)
-      | intros.
-        apply (le_S_S O m).
-        apply (le_O_n m)
-      ]
-    | assumption
-    ]
-  | apply (lt_times_eq_O d (a - (S O)));
-      assumption
-  ]
-| apply (plus_to_minus ).
+apply (inj_times_r1 d)
+[ assumption
+| rewrite > sym_times.
+  rewrite < (times_n_SO d).
   assumption
 ]
-qed.
+qed.*)
+
 
 theorem div_mod_minus:
 \forall a,b:nat. O \lt b \to
 (a /b)*b = a - (a \mod b).
 intros.
-apply sym_eq.
-apply (inj_plus_r (a \mod b)).
-rewrite > (sym_plus (a \mod b) ?).
-rewrite < (plus_minus_m_m a (a \mod b))
-[ rewrite > sym_plus.
-  apply div_mod.
-  assumption
-| rewrite > (div_mod a b) in \vdash (? ? %)
-  [ rewrite > plus_n_O in \vdash (? % ?).
-    rewrite > sym_plus.
-    apply cic:/matita/nat/le_arith/le_plus_n.con
-  | assumption
-  ]
+rewrite > (div_mod a b) in \vdash (? ? ? (? % ?))
+[ apply (minus_plus_m_m (times (div a b) b) (mod a b))
+| assumption
 ]
 qed.
 
+(*
 theorem sum_div_eq_div: \forall a,b,c:nat.
 O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
 intros.
@@ -283,7 +190,7 @@ rewrite > (div_plus_times c n2 b)
 | assumption
 ]
 qed.
-
+*)
 
 (* A corollary to the division theorem (between natural numbers).
  *
@@ -308,83 +215,74 @@ split
 | rewrite < (times_n_Sm b c).
   rewrite < H1.
   rewrite > sym_times.
-  rewrite > div_mod_minus
-  [ rewrite < (eq_minus_plus_plus_minus b a (a \mod b))
-    [ rewrite < (sym_plus a b).
-      rewrite > (eq_minus_plus_plus_minus a b (a \mod b))
-      [ rewrite > (plus_n_O a) in \vdash (? % ?).
-        apply (le_to_lt_to_plus_lt)
-        [ apply (le_n a)
-        | apply cic:/matita/nat/minus/lt_to_lt_O_minus.con.      
-          apply cic:/matita/nat/div_and_mod/lt_mod_m_m.con.
-          assumption
-        ]
-      | apply lt_to_le.
-        apply lt_mod_m_m.
-        assumption
-      ]
-    | rewrite > (div_mod a b) in \vdash (? ? %)
-      [ rewrite > plus_n_O in \vdash (? % ?).
-        rewrite > sym_plus.
-        apply cic:/matita/nat/le_arith/le_plus_n.con
-      | assumption
-      ]
-    ]
+  rewrite > (div_mod a b) in \vdash (? % ?)
+  [ rewrite > (sym_plus b ((a/b)*b)).
+    apply lt_plus_r.
+    apply lt_mod_m_m.
+    assumption
   | assumption
   ]
 ]
 qed.
+  
 
 theorem th_div_interi_1: \forall a,c,b:nat.
 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
 intros.
 apply (le_to_le_to_eq)
-[ cut (a/b \le c \lor c \lt a/b)
-  [ elim Hcut
-    [ assumption
-    | change in H3 with ((S c) \le (a/b)).
-      cut (b*(S c) \le (b*(a/b)))
-      [ rewrite > (sym_times b (S c)) in Hcut1.
-        cut (a \lt (b * (a/b)))
-        [ rewrite > (div_mod a b) in Hcut2:(? % ?)
-          [ rewrite > (plus_n_O (b*(a/b))) in Hcut2:(? ? %).
-            cut ((a \mod b) \lt O)
-            [ apply False_ind.
-              apply (lt_to_not_le (a \mod b) O)
-              [ assumption
-              | apply le_O_n
-              ]              
-            | apply (lt_plus_to_lt_r ((a/b)*b)).
-              rewrite > (sym_times b (a/b)) in Hcut2:(? ? (? % ?)).
-              assumption 
-            ]
-          | assumption
-          ]
-        | apply (lt_to_le_to_lt ? (b*(S c)) ?)
+[ apply (leb_elim (a/b) c);intros
+  [ assumption
+  | cut (c \lt (a/b))
+    [ apply False_ind.
+      apply (lt_to_not_le (a \mod b) O)
+      [ apply (lt_plus_to_lt_l ((a/b)*b)).
+        simplify.
+        rewrite < sym_plus.
+        rewrite < div_mod
+        [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
           [ assumption
-          | rewrite > (sym_times b (S c)).
+          | rewrite > (sym_times (a/b) b).
+            apply le_times_r.
             assumption
           ]
+        | assumption
         ]
-      | apply le_times_r.
-        assumption
+      | apply le_O_n
       ]
-    ]
-  | apply (leb_elim (a/b) c)
-    [ intros.
-      left.
+    | apply not_le_to_lt.
       assumption
-    | intros.
-      right.
-      apply cic:/matita/nat/orders/not_le_to_lt.con. 
+    ]
+  ]
+| apply (leb_elim c (a/b));intros
+  [ assumption
+  | cut((a/b) \lt c) 
+    [ apply False_ind.
+      apply (lt_to_not_le (a \mod b) b)
+      [ apply (lt_mod_m_m).
+        assumption
+      | apply (le_plus_to_le ((a/b)*b)).
+        rewrite < (div_mod a b)
+        [ apply (trans_le ? (b*c) ?)
+          [ rewrite > (sym_times (a/b) b).
+            rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
+            rewrite < distr_times_plus.
+            rewrite > sym_plus.
+            simplify in \vdash (? (? ? %) ?).
+            apply le_times_r.
+            assumption
+          | assumption
+          ]
+        | assumption
+        ]
+      ]
+    | apply not_le_to_lt. 
       assumption
     ]
-  ] 
-| apply (bTIMESc_le_a_to_c_le_aDIVb);
-    assumption
+  ]
 ]
 qed.
 
+
 theorem times_numerator_denominator_aux: \forall a,b,c,d:nat.
 O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c).
 intros.