X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fpi_p.ma;h=0c5e0d7014bda9cfcc98fb061738499b726d5211;hb=98c84d48f4511cb52c8dc03881e113bd4bd9c6ce;hp=9e820cd79bd2d5469f961a5cec32daaaae7e3147;hpb=3f5a0152427fd9a89e7239befd259d27b97aaef5;p=helm.git

diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index 9e820cd79..0c5e0d701 100644
--- a/helm/software/matita/library/nat/pi_p.ma
+++ b/helm/software/matita/library/nat/pi_p.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/pi_p".
-
 include "nat/primes.ma".
 (* include "nat/ord.ma". *)
 include "nat/generic_iter_p.ma".
@@ -200,17 +198,16 @@ theorem le_pi_p:
 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to 
 pi_p n p g1 \le pi_p n p g2.
 intros.
-generalize in match H.
-elim n
+elim n in H ⊢ %
   [apply le_n.
   |apply (bool_elim ? (p n1));intros
     [rewrite > true_to_pi_p_Sn
       [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
         [apply le_times
-          [apply H2[apply le_n|assumption]
-          |apply H1.
+          [apply H1[apply le_n|assumption]
+          |apply H.
            intros.
-           apply H2[apply le_S.assumption|assumption]
+           apply H1[apply le_S.assumption|assumption]
           ]
         |assumption
         ]
@@ -218,9 +215,9 @@ elim n
       ]
     |rewrite > false_to_pi_p_Sn
       [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
-        [apply H1.
+        [apply H.
          intros.
-         apply H2[apply le_S.assumption|assumption]
+         apply H1[apply le_S.assumption|assumption]
         |assumption
         ]
       |assumption