(* *)
(**************************************************************************)
-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
]
qed.
+theorem exp_sigma_p1: \forall n,a,p,f.
+pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
+intros.
+elim n
+ [reflexivity
+ |apply (bool_elim ? (p n1))
+ [intro.
+ rewrite > true_to_pi_p_Sn
+ [rewrite > true_to_sigma_p_Sn
+ [simplify.
+ rewrite > H.
+ rewrite > exp_plus_times.
+ reflexivity.
+ |assumption
+ ]
+ |assumption
+ ]
+ |intro.
+ rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_sigma_p_Sn
+ [simplify.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
theorem times_pi_p: \forall n,p,f,g.
pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p g.
intros.