Non working parts of the library commented out.

[helm.git] / matita / matita / lib / arithmetics / binomial.ma

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 9397f7b4dd7241abec546b34b0f3be8c2261d169..c31e15d112ea510955481ef32e059a7c5584cc83 100644 (file)
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -89,6 +89,7 @@ theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
   ]
 qed. 
 
+(*
 theorem binomial_law:∀a,b,n.
   (a+b)^n = Σ_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
 #a #b #n (elim n) //
@@ -130,4 +131,4 @@ rewrite < assoc_plus.
 rewrite < sym_plus.
 reflexivity.
 qed. *)
-
+*)
\ No newline at end of file