Bertrand's conjecture (weak), some work in progress

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

diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma
index 4434f769b29e526b0de535836e4abfd9f6a0fdd0..9505761488e3dd9568d51036ff877471c21215de 100644 (file)
--- 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