X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fsigma_pi.ma;h=8d2a5858ab2d842302cc873c1756c3008ce9d5cc;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hp=7e3fe19f04df5f44b586f815b8afeaa74312a24a;hpb=b5f51e592232d16fb1286f059a597c8ab443b4c4;p=helm.git

diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
index 7e3fe19f0..8d2a5858a 100644
--- a/matita/matita/lib/arithmetics/sigma_pi.ma
+++ b/matita/matita/lib/arithmetics/sigma_pi.ma
@@ -186,3 +186,14 @@ theorem exp_sigma_l: ∀n,a,p,f.
   |>bigop_Sfalse [>bigop_Sfalse [@Hind|//] | //]
   ]
 qed.
+
+theorem exp_pi_l: ∀n,a,f. 
+  exp a n*(∏_{i < n}(f i)) = ∏_{i < n} (a*(f i)).
+#n #a #f elim n // #i #Hind >bigop_Strue // >bigop_Strue //
+<Hind <associative_times <associative_times @eq_f2 // normalize // 
+qed.
+
+theorem exp_pi_bc: ∀a,b,c,f. 
+  exp a (c-b)*(∏_{i ∈ [b,c[ }(f i)) = ∏_{i ∈ [b,c[ } (a*(f i)).
+#a #b #c #f @exp_pi_l 
+qed.
\ No newline at end of file