X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ffactorization.ma;h=bfdf947b4ba1ec437d1520b4095bd01a1320e54c;hb=73a66cce6e72c654fdcd0ce760c405a74af70d08;hp=6226f3b6de81997ac3eefa61006d0c54205deafc;hpb=37f225a76270658463fb28f9d2619efcecabdcd2;p=helm.git

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index 6226f3b6d..bfdf947b4 100644
--- a/helm/software/matita/library/nat/factorization.ma
+++ b/helm/software/matita/library/nat/factorization.ma
@@ -61,13 +61,10 @@ cut (\exists i. nth_prime i = smallest_factor n);
       [ apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | apply lt_SO_smallest_factor; assumption; ]
-      | letin x \def le.autobatch.
-         (*       
-       apply divides_smallest_factor_n;
-        apply (trans_lt ? (S O));
-        [ unfold lt; apply le_n;
-        | assumption; ] *) ] ]
-  | autobatch. 
+      | apply divides_smallest_factor_n;
+        autobatch; ] ]
+  | apply prime_to_nth_prime;
+    autobatch. 
     (* 
     apply prime_to_nth_prime;
     apply prime_smallest_factor_n;
@@ -156,27 +153,22 @@ apply divides_max_prime_factor_n.
 assumption.unfold Not.
 intro.
 cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
-  [unfold Not in Hcut1.autobatch.
+  [ apply Hcut1; autobatch depth=2;
     (*
     apply Hcut1.apply divides_to_mod_O;
     [ apply lt_O_nth_prime_n.
     | assumption.
     ]
     *)
-  |letin z \def le.
-   cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
-   [2: rewrite < H1.assumption.|letin x \def le.autobatch width = 4 depth = 2]
-   (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
-  ].
-(*
-    apply (p_ord_aux_to_not_mod_O n n ? q r);
+  | unfold p_ord in H2; lapply depth=0 le_n; autobatch width = 4 depth = 2; 
+    (*apply (p_ord_aux_to_not_mod_O n n ? q r);
     [ apply lt_SO_nth_prime_n.
     | assumption.
     | apply le_n.
     | rewrite < H1.assumption.
-    ]
+    ]*)
   ].
-*)  
+  
 apply (le_to_or_lt_eq (max_prime_factor r)  (max_prime_factor n)).
 apply divides_to_max_prime_factor.
 assumption.assumption.
@@ -526,7 +518,7 @@ split
       [apply lt_O_nth_prime_n
       |apply (lt_O_n_elim ? H).
        intro.
-       apply (witness ? ? (r*(nth_prime p \sup m))).
+       apply (witness ? ? ((r*(nth_prime p) \sup m))).
        rewrite < assoc_times.
        rewrite < sym_times in \vdash (? ? ? (? % ?)).
        rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).