X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fpi_p.ma;h=93f127372410610e5147fe02c5bf3fa59a08b2c7;hb=2a31f145f58f7ba66b6445a9c8b31841054ef809;hp=e649f5f193ecdda0b0d9e7fc0c54b0d7355a233c;hpb=6db38e3d8e4083765f2fce40c7845c9827b9afd0;p=helm.git

diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index e649f5f19..93f127372 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".
@@ -257,6 +255,35 @@ elim n
   ]
 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.