huge commit in automation:

[helm.git] / helm / software / matita / library / nat / factorization.ma

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index 92f64e56d9a9c7a556a21f1cacd6d60edaf3b81e..bfdf947b4ba1ec437d1520b4095bd01a1320e54c 100644 (file)
--- 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.