(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/pi_p".
-
include "nat/primes.ma".
(* include "nat/ord.ma". *)
include "nat/generic_iter_p.ma".
(\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
]
]
|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