Prima versione di bertrand. Tanti cambiamenti qua e la.

[helm.git] / helm / software / matita / library / nat / pi_p.ma

diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
index e649f5f193ecdda0b0d9e7fc0c54b0d7355a233c..9e820cd79bd2d5469f961a5cec32daaaae7e3147 100644 (file)
--- a/helm/software/matita/library/nat/pi_p.ma
+++ b/helm/software/matita/library/nat/pi_p.ma
@@ -257,6 +257,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.