First attempt at using/simulating records with manifest types to encode

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

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index fc9352e12395cbb117af7054f01b17bc41d1c38d..85351c06d47ac9b63e5d4a94964d7d6e56f97a9c 100644 (file)
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -46,13 +46,13 @@ intros; apply divides_b_true_to_divides;
       [ apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | apply lt_SO_smallest_factor; assumption; ]
-      | letin x \def le.auto.
+      | letin x \def le.auto new.
          (*       
        apply divides_smallest_factor_n;
         apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | assumption; ] *) ] ]
-  | letin x \def prime. auto.
+  | auto. 
     (* 
     apply prime_to_nth_prime;
     apply prime_smallest_factor_n;
@@ -105,7 +105,7 @@ 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.auto.
+  [unfold Not in Hcut1.auto new.
     (*
     apply Hcut1.apply divides_to_mod_O;
     [ apply lt_O_nth_prime_n.
@@ -114,7 +114,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]
+   [2: rewrite < H1.assumption.|letin x \def le.auto width = 4 new]
    (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
   ].
 (*