X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgeneric_iter_p.ma;h=4796ec10b2e14c1829daefba403a11b34e98e38d;hb=b771a37f83637be22d9b3f1254a6a0f15dc49612;hp=f89c32f870c6f4dfe26fd4406ce8a7079a3ea39f;hpb=5e50ef5a9b00a18778c0eb728f7fc909c0b0f729;p=helm.git

diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma
index f89c32f87..4796ec10b 100644
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/generic_iter_p".
-
 include "nat/div_and_mod_diseq.ma".
 include "nat/primes.ma".
 include "nat/ord.ma".
@@ -1573,7 +1571,10 @@ apply (trans_eq ? ?
                 [ assumption
                 | assumption
                 ]
-              | rewrite > H14.
+              | unfold ha.
+                unfold ha12.
+                unfold ha22.
+                rewrite > H14.
                 rewrite > H13.
                 apply sym_eq.
                 apply div_mod.
@@ -1620,18 +1621,23 @@ apply (trans_eq ? ?
                 rewrite > Hcut.
                 assumption
               ] 
-            | rewrite > Hcut1.
+            | unfold ha.
+              unfold ha12.
+              rewrite > Hcut1.
               rewrite > Hcut.
               assumption
             ]
-          | rewrite > Hcut1.
+          | unfold ha.
+            unfold ha22.
+            rewrite > Hcut1.
             rewrite > Hcut.
             assumption            
           ]
         | cut(O \lt m1)
           [ cut(O \lt n1)      
             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
-              [ apply (lt_plus_r).
+              [ unfold ha.
+                apply (lt_plus_r).
                 assumption
               | rewrite > sym_plus.
                 rewrite > (sym_times (h11 i j) m1).
@@ -1757,7 +1763,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y
     |assumption
     ]
   ]
-qed.
-
-
-
+qed.
\ No newline at end of file