X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbinomial.ma;h=c3834c8d847b8d001f48ef19217b9d121e1a2944;hb=be80aa40b9a66d5b12f92d03c2aa7b1dd8e49893;hp=74d2c8efd5ad9ecda487fe89cd5e618d50cc3fbb;hpb=90293a04a41156a66b381a867714d3563b4c2594;p=helm.git

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 74d2c8efd..c3834c8d8 100644
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -191,13 +191,3 @@ cut (2 = 1+1) [//] #H2 >H2 in ⊢ (??(?%?));
   ]
 qed.
       
-(*
-theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
-intros.simplify.
-rewrite < times_n_SO.
-rewrite < plus_n_O.
-rewrite < sym_times.simplify.
-rewrite < assoc_plus.
-rewrite < sym_plus.
-reflexivity.
-qed. *)