Restructuring.

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

diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index ea306f4554a6c2c83e809dace78d034d9534bcc8..c5236ff4a6f8678907c1143bf47ffd18d5c1dcf5 100644 (file)
--- 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.