deps fixed

[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 37a7045924540be5f718043bc79eba2c3c742842..f5b147005f84ff8b9490bff1f66ec44a04524192 100644 (file)
--- a/helm/software/matita/library/nat/factorization.ma
+++ b/helm/software/matita/library/nat/factorization.ma
@@ -125,7 +125,7 @@ cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
     *)
   |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.auto width = 4 new]
+   [2: rewrite < H1.assumption.|letin x \def le.auto width = 4 depth = 2]
    (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
   ].
 (*
@@ -399,7 +399,6 @@ apply (not_eq_O_S (S m1)).
 rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
 apply le_to_or_lt_eq.apply le_O_n.
 (* prova del cut *)
-goal 20.
 apply (p_ord_aux_to_exp (S(S m1))).
 apply lt_O_nth_prime_n.
 assumption.