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 6bcd62a653b38465021da0bb395700089e4afd70..d6b462b10dbbc61bcf44d8e9f2b9c1a9727b9744 100644 (file)
--- 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 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

diff --git a/matita/matita/lib/arithmetics/nth_prime.ma b/matita/matita/lib/arithmetics/nth_prime.ma
index 7b7c70bfe5cabfca704dce146034cb3ff1abad88..c973d0b12a272f74630310410960539b84acd8e1 100644 (file)
--- 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 d92d525b7c37b9c5c200c6f5a6ffc15db8a974b5..94b3794b3f08345bad1d83896e5b88ed2d737f43 100644 (file)
--- 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