auto rewritten with only one tail recursive function.

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

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 826a2670a70a6c80822c2baeb4764962822af120..f5b147005f84ff8b9490bff1f66ec44a04524192 100644 (file)
--- a/matita/library/nat/factorization.ma
+++ b/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 *)
   ].
 (*