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