X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fbinomial.ma;h=9505761488e3dd9568d51036ff877471c21215de;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=4434f769b29e526b0de535836e4abfd9f6a0fdd0;hpb=892992b24f5476c2b4eed13f64e04854ef919020;p=helm.git

diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma
index 4434f769b..950576148 100644
--- a/helm/software/matita/library/nat/binomial.ma
+++ b/helm/software/matita/library/nat/binomial.ma
@@ -213,4 +213,17 @@ intros.elim n
             |reflexivity]]
       |reflexivity]
    |reflexivity]]
+qed.
+
+theorem exp_S_sigma_p:\forall a,n.
+exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
+intros.
+rewrite > plus_n_SO.
+rewrite > exp_plus_sigma_p.
+apply eq_sigma_p;intros
+  [reflexivity
+  |rewrite < exp_SO_n.
+   rewrite < times_n_SO.
+   reflexivity
+  ]
 qed.
\ No newline at end of file