X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fsigma_pi.ma;h=8d2a5858ab2d842302cc873c1756c3008ce9d5cc;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hp=32153b352ca55968b272c4c0716c5f50a43cbdbd;hpb=90293a04a41156a66b381a867714d3563b4c2594;p=helm.git

diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
index 32153b352..8d2a5858a 100644
--- a/matita/matita/lib/arithmetics/sigma_pi.ma
+++ b/matita/matita/lib/arithmetics/sigma_pi.ma
@@ -178,3 +178,22 @@ theorem exp_pi: ∀n,m,p,f.
   |#m1 #Hind >times_pi >Hind %
   ]
 qed.
+
+theorem exp_sigma_l: ∀n,a,p,f. 
+  ∏_{i < n | p i} (exp a (f i)) = exp a (∑_{i < n | p i}(f i)).
+#n #a #p #f elim n // #i #Hind cases (true_or_false (p i)) #Hc
+  [>bigop_Strue [>bigop_Strue [>Hind >exp_plus_times // |//] |//]
+  |>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