X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fiteration2.ma;h=c5236ff4a6f8678907c1143bf47ffd18d5c1dcf5;hb=5e50ef5a9b00a18778c0eb728f7fc909c0b0f729;hp=ea306f4554a6c2c83e809dace78d034d9534bcc8;hpb=1f214ad28b490ed66602eb2d80359c01ba55ee05;p=helm.git

diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index ea306f455..c5236ff4a 100644
--- a/helm/software/matita/library/nat/iteration2.ma
+++ b/helm/software/matita/library/nat/iteration2.ma
@@ -191,6 +191,20 @@ apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
 ]
 qed.
 
+theorem eq_sigma_p_pred: 
+\forall n,p,g. p O = true \to
+sigma_p (S n) (\lambda i.p (pred i)) (\lambda i.g(pred i)) = 
+plus (sigma_p n p g) (g O).
+intros.
+unfold sigma_p.
+apply eq_iter_p_gen_pred
+  [assumption
+  |apply symmetricIntPlus
+  |apply associative_plus
+  |intros.apply sym_eq.apply plus_n_O
+  ]
+qed.
+
 (* monotonicity *)
 theorem le_sigma_p: 
 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.