From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 Nov 2011 17:50:21 +0000 (+0000)
Subject: Non working parts of the library commented out.
X-Git-Tag: make_still_working~2101
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2983f88c7fedc8973e1104322fa884fb6b3cfb30;p=helm.git

Non working parts of the library commented out.
---

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 6bcd62a65..d6b462b10 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -174,7 +174,7 @@ theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat →
   [>bigop_Strue // >Hind >bigop_sum @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
    #eqi [|#H] (>eqi in ⊢ (???%))
-     >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/
+     >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize //
   |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
    #eqi >eqi in ⊢ (???%) >div_plus_times /2/ 
diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 9397f7b4d..c31e15d11 100644
--- 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
diff --git a/matita/matita/lib/arithmetics/nth_prime.ma b/matita/matita/lib/arithmetics/nth_prime.ma
index 7b7c70bfe..c973d0b12 100644
--- a/matita/matita/lib/arithmetics/nth_prime.ma
+++ b/matita/matita/lib/arithmetics/nth_prime.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* To be ported
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
 
@@ -198,4 +199,4 @@ apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.
 simplify.unfold prime in H.elim H.assumption.
 qed.
-
+*)
\ No newline at end of file
diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
index d92d525b7..94b3794b3 100644
--- a/matita/matita/lib/arithmetics/sigma_pi.ma
+++ b/matita/matita/lib/arithmetics/sigma_pi.ma
@@ -9,6 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
+(* To be ported
 include "arithmetics/bigops.ma".
 
 definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 
@@ -744,4 +745,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y
     |assumption
     ]
   ]
-qed. *)
\ No newline at end of file
+qed. *)*)
\ No newline at end of file