Theory Chebyshev2

(*  Title:      Chebyshev2.thy
    Author:     Paul Raff and Jeremy Avigad
*)

theory Chebyshev2 = Chebyshev1:

declare binomial_Suc_Suc [simp del];

(* important lemmas for general use *)

subsection {* General facts -- move some of these into libraries! *}

lemma setsum_multiplier: "finite A ==> (k::nat)*(setsum f  A) = setsum (%i. k*f(i)) A";
  apply (induct set: Finites);
  apply force;
  apply (simp add: setsum_insert);
  apply (simp add: add_mult_distrib2);
done;

lemma setsum_multiplier_real: "finite A ==> (k::real)*(setsum f A) = setsum (%i. k * f(i)) A";
  apply (induct set: Finites);
  apply force;
  apply (simp add: setsum_insert);
  apply (subst mult_commute);back;
  apply (subst real_add_mult_distrib);
  apply auto;
  apply (subst mult_commute);
  apply assumption;
  done;

lemma empty_interval [simp]: "{Suc b..b} = {}";
  apply auto;
  done;

lemma interval1 [simp]: "{(a::nat)..a} = {a}";
  by auto;

lemma interval2 [simp]: "{(a::nat)..a(} = {}";
  by auto;

lemma interval3 [simp]: "{)(a::nat)..a} = {}";
  by auto;

lemma insert_interval: "{(0::nat)..Suc n(} = insert n {..n(}";
  apply auto;
done;

lemma right_open_prop: "n ~: {(0::nat)..n(}";
  apply auto;
done;

lemma right_closed_prop: "Suc n ~: {(0::nat)..n}";
  by auto;

lemma insert_interval_closed: "{(0::nat)..Suc n} = insert (Suc n) {..n}";
  by auto;

lemma setsum_interval_insert: "setsum f {0..Suc n(} = setsum f {0..n(} + f n";
  apply (auto simp add:insert_interval right_open_prop setsum_insert);
  apply (subgoal_tac "{..n(} = {0..n(}");
  apply (erule ssubst);
  apply auto;
  apply (simp only: plus_ac0);
done;

lemma setsum_interval_insert_closed: "setsum f {0..Suc n} = setsum f {0..n} + f (Suc n)";
  apply (auto simp add: insert_interval_closed right_closed_prop setsum_insert);
  apply (subgoal_tac "{..n} = {0..n}");
  apply (erule ssubst);
  apply (auto simp add: plus_ac0);
done;

lemma setsum_index_shift_right: "setsum f {(0::nat)..b} = setsum (%i. f(i-k)) {k..(b+k)}";
  apply (induct_tac b);
  apply force;
  apply (simp only: setsum_interval_insert_closed);
  apply (subgoal_tac "(Suc n + k) ~: {k..n+k}");
  apply (subgoal_tac "{k..Suc n + k} = insert (Suc n + k) {k..n+k}");
  apply (simp add: setsum_insert);
  apply (auto simp add: plus_ac0);
done;

lemma setsum_index_shift_left: "a<= b ==> setsum f {(a::nat)..b} = setsum (%i. f(a+i)) {0..(b-a)}";
  apply (simp add: setsum_index_shift_right [of "(%i. f(a+i))" "b-a" "a"]);
  apply (subgoal_tac "(∑i::nat:{a..b}. f (a + (i - a))) = (∑i::nat:{a..b}. f(i))");
  apply (erule ssubst);
  apply force;
  apply (rule setsum_cong);
  apply auto;
done;

lemma real_nat_division: "0 < b ==> a mod b = (0::nat) ==> real(a div b) = real(a)/real(b)";
  apply (subgoal_tac "0 < real(b)");
  apply (simp add: nonzero_eq_divide_eq);
  apply (simp only: times_ac1 real_of_nat_mult [THEN sym]);
  apply (simp only: mult_div_cancel);
  apply auto;
done;

lemma div_combine: "a mod b = (0::nat) ==> (c * (a div b)) = ((c*a) div b)";
  apply auto;
done;  

lemma div_combine_2: "c mod b = (0::nat) ==> (a * (c div b)) = ((c*a) div b)";
  apply auto;
  done;

lemma nat_le_diff: "(x::nat) <= y - k ==> x <= y";
  apply (case_tac "y <= k");
  apply force;
  apply (case_tac "y = k");
  apply force;
  apply (subgoal_tac "k < y");
  apply auto;
  apply (subgoal_tac "x + k <= y - k + k");
  apply (subgoal_tac "k <= y");
  apply (simp add: le_add_diff_inverse2);
  apply force+;
  apply (simp only: add_le_mono1 [of _ _ "k"]);
done;

lemma div_add: "a mod c = (0::nat) ==> b mod c = 0 ==> (a div c + b div c) = ((a+b) div c)";
  apply (simp add: div_add1_eq);
done;

lemma factorial_never_0 [simp]: "fact(n) ~= 0";
  by simp;

lemma factorial_gt_0 [simp]: "0 < fact n";
  apply simp;
  done;

lemma product_eq: "a ~= 0 ==> b ~= 0 ==> d ~= 0 ==> (a::nat)*b*c = d ==> a*b*e = d ==> c = e";
  apply auto;
done;

lemma factorial_pos: "1 <= k ==> fact k = k * fact(k - 1)";
  apply (case_tac k);
  apply auto;
done;

lemma product_div: "0 < (b::nat) ==> a * b = c ==> a = c div b";
  apply auto;
  done;

lemma lt_gt_product: "0 < a ==> 0 < b ==>  0 < d ==> (a::nat) * b = c * d ==> a < c ==> (d < b)";
  proof-;
    assume a: "0 < a";
    assume b: "0 < b";
    assume d: "0 < d";
    assume eq: "a * b = c * d";
    assume ineq1: "a < c";
    have step1: "a * b * d < c * b * d";
      apply (auto);
      apply (auto simp add: d b ineq1);
      done;
    from step1; have step2: "c * d * d < c * b * d"; 
      apply (simp add: eq);
      done;
    from step2; have step3: "d * d < b * d";
      apply auto;
      done;
    also from step3 show ?thesis;
      apply auto;
      done;
    qed;

lemma gt_lt_product: "0 < a ==> 0 < c ==> 0 < d ==> (a::nat) * b = c * d ==> d < b ==> (a < c)";
  proof-;
    assume a: "0<a";
    assume c: "0<c";
    assume d: "0<d";
    assume eq: "a*b = c*d";
    assume ineq: "d < b";
    have step1: "a * d * c < a * b * c";
      apply auto;
      apply (auto simp add: a c ineq);
      done;
    from step1 have step2: "a * d * c < c * d * c";
      apply (simp only: eq);
      done;
    from step2 have step3: "a * d < c * d";
      apply auto;
      done;
    from step3 show ?thesis;
      by auto;
    qed;

lemma gt_lt_product_iff: "0 < a ==> 0 < b ==> 0 < c ==> 0 < d ==> (a::nat) * b = c * d ==> (d < b) = (a < c)";
  apply (auto);
  apply (force intro: gt_lt_product, force intro: lt_gt_product);
done;

lemma eq_product_iff: "0 < a ==> 0 < b ==> 0 < c ==> 0 < d ==> (a::nat) * b = c * d ==> (d = b) = (a = c)";
  apply auto;
done;

lemma nat_less_diff: "(a < b - (c::nat)) = (a + c < b)";
  apply (induct b c rule: diff_induct);
  apply auto;
done;

lemma sum_greater_than_part: "finite A ==> a : A ==> 
    ALL x:A. (0 < (f(x)::nat)) ==> (A - {a}) ~= {} ==>
                              f(a) < setsum f A";
  apply (subgoal_tac "A = insert a (A - {a})");
  apply (erule ssubst);
  apply (subst setsum_insert);
  apply force+;
done;

lemma setsum_constant_bound: "finite A ==> ALL x:A. (f(x) <= k) ==> setsum f A <= card(A)*k";
  apply (induct set: Finites);
  apply force;
  apply (auto simp add: setsum_insert);
done;

lemma chained_inequalities_up [rule_format]: "(ALL i < n. ((f(i)::nat) < f(Suc i))) --> k < n --> f(k) < f(n)";
  apply (induct_tac n);
  apply force;
  apply (simp only: le_simps);
  apply (rule impI);
  apply (rule impI);
  apply auto;
  apply (subgoal_tac "k = n");
  apply (frule_tac x = "n" in spec);
  apply (subgoal_tac "n <= n");
  apply (frule mp);
  apply auto;
done;

lemma chained_inequalities_down [rule_format]: "(ALL i < n. f(Suc i) < (f(i)::nat)) --> k < n --> f(Suc k) < f(0)";
  apply (induct_tac k);
  apply force;
  apply force;
done;


lemma sum_is_greater_than_part: "finite A ==> B <= A ==> ALL x:A. (0 < (f(x)::nat)) ==> A - B ~= {} ==> setsum f B < setsum f A";
  apply (subgoal_tac "A = B Un (A - B)");
  apply (erule ssubst);
  apply (subgoal_tac "finite B");
  apply (subgoal_tac "finite (A - B)");
  apply (frule setsum_Un_disjoint [of "B" "A - B" "f"]);
  apply force+;
  apply (simp add: finite_subset);
  apply force;
  done;

lemma setprod_dvd: "finite A ==> (x::nat):A ==> x dvd setprod id A";
  apply (induct set: Finites);
  apply force;
  apply (simp add: setprod_insert);
  apply auto;
  apply (simp add: dvd_mult);
  done;
  
lemma prime_divides_product: "m+2 <= p ==> p <= Suc(2*m) ==> p dvd setprod id {m+2..Suc(2*m)}";
  by (rule setprod_dvd, auto);

lemma factorial_Suc: "fact n + n * fact n = fact (Suc n)";
  apply auto;
  done;

lemma primes_dvd_one_or_other_left: "a : prime ==> (a::nat) dvd b*c ==> ~ (a dvd b) ==> a dvd c";
  apply (frule prime_dvd_mult);
  apply auto;
  done;

lemma primes_dvd_one_or_other_right: "a : prime ==> (a::nat) dvd b*c ==> ~ (a dvd c) ==> a dvd b";
  apply (frule prime_dvd_mult, auto);
  done;

lemma prime_dividing_factorial [rule_format]: "p : prime --> p dvd fact n --> p <= n";
  apply (induct_tac n);
  apply (simp add: prime_def);
  apply auto;
  apply (simp only: factorial_Suc);
  apply (simp only: fact_Suc);
  apply (subgoal_tac "p dvd Suc n");
  apply (rule dvd_imp_le);
  apply force;
  apply force;
  apply (rule primes_dvd_one_or_other_right);
  apply auto;
  done;

lemma prime_not_divide_less: "p : prime ==> m+2 <= p ==> p <= Suc(2*m) ==> ~ p dvd fact(m)";
  apply (rule contrapos_pn);
  apply auto;
  apply (frule prime_dividing_factorial);
  apply auto;
  done;

lemma factorial_setprod_def: "fact n = setprod id {1..n}";
  apply (induct_tac n);
  apply (simp only: fact_0);
  apply (subgoal_tac "{1..0} = {}");
  apply (erule ssubst);
  apply force;
  apply force;
  apply (simp only: fact_Suc);
  apply (subgoal_tac "{1..Suc n} = {1..n} Un {Suc n}");
  apply (subgoal_tac "finite {1..n}");
  apply (subgoal_tac "finite {Suc n}");
  apply (subgoal_tac "{1..n} Int {Suc n} = {}");
  apply (simp only: setprod_Un_disjoint);
  apply (subgoal_tac "setprod id {1..n} = fact n");
  apply (erule ssubst);back;back;back;
  apply simp;
  apply (simp only: nat_mult_commute);
  apply force+;
  done;

lemma setprod_interval_insert_1: "setprod f {1..Suc n} = setprod f {1..n} * (f(Suc n)::'a::semiring)";
  apply (subgoal_tac "{1..Suc n} = {1..n} Un {Suc n}");
  apply (erule ssubst);
  apply (subgoal_tac "finite {1..n}");
  apply (subgoal_tac "finite {Suc n}");
  apply (simp add: setprod_Un_disjoint);
  apply auto;
  apply (simp add: mult_ac);
  done;

lemma setprod_interval_insert: "b <= Suc a ==> setprod f {b..Suc a} = setprod f {b..a} * (f(Suc a)::'a::semiring)";
  apply (subgoal_tac "{b..Suc a} = {b..a} Un {Suc a}");
  apply (erule ssubst);
  apply (subgoal_tac "finite {b..a}");
  apply (subgoal_tac "finite {Suc a}");
  apply (simp add: setprod_Un_disjoint);
  apply (auto simp add: mult_ac);
  done;
  
lemma setprod_interval_gt_0 [rule_format]: "0 < b ==> b <= a --> 0 < setprod id {b..(a::nat)}";
  apply (induct_tac a);
  apply force;
  apply auto;
  apply (subgoal_tac "b = Suc n");
  apply (erule ssubst);
  apply force+;
  apply (subst setprod_interval_insert);
  apply force+;
  done;

lemma setprod_interval_1_gt_0 [simp]: "0 < setprod id {1..(n::nat)}";
  apply (case_tac n);
  apply force;
  apply (rule setprod_interval_gt_0);
  apply force+;
  done;

lemma setprod_interval_Suc0_gt_0 [simp]: "0 < setprod id {Suc 0..(n::nat)}";
  apply (subgoal_tac "Suc 0 = 1");
  apply (erule ssubst);
  apply (simp only: setprod_interval_1_gt_0);
  by force;

lemma setprod_interval_multiply [rule_format]: "a <= b --> setprod id {1..b} = setprod id {1..a} * setprod id {Suc a..b}";
  apply (induct_tac b);
  apply (rule impI);
  apply (subgoal_tac "a = 0");
  apply (erule ssubst);
  apply (subgoal_tac "{1..0} = {}");
  apply (erule ssubst);
  apply (subgoal_tac "{Suc(0)..0} = {}");
  apply (erule ssubst);
  apply force+;
  apply (rule impI);
  apply (case_tac "a <= n");
  apply (frule mp);
  apply force;
  apply (subgoal_tac "setprod id {1::nat..Suc n} = setprod id {1::nat..n} * id (Suc n)");
  apply (erule ssubst);back;
  apply (erule ssubst);
  apply (subgoal_tac "setprod id {Suc a..n} * id (Suc n) = setprod id {Suc a..Suc n}");
  apply (subst nat_mult_assoc);
  apply (erule ssubst);
  apply (force);
  apply (subgoal_tac "setprod id {Suc a..Suc n} = setprod id {Suc a..n} * id (Suc n)");
  apply force;
  apply (subgoal_tac "Suc a <= Suc n");
  apply (simp only: setprod_interval_insert);
  apply force+;
  apply (simp only: setprod_interval_insert);
  apply (subgoal_tac "a = Suc n");
  apply (erule ssubst);
  apply (subgoal_tac "{Suc (Suc n)..Suc n} = {}");
  apply (erule ssubst);
  apply force+;
  done;

lemma setprod_interval_mod: "a <= b ==> setprod id {1..b} mod setprod id {1..(a::nat)} = 0";
  apply (simp only: mod_eq_0_iff);
  apply (rule_tac x = "setprod id {Suc a..b}" in exI);
  apply (simp only: setprod_interval_multiply);
  done;

lemma div_multiply: "0 < b ==> 0 < c ==> ((a::nat) = b*c) ==> (b = a div c)";
  apply auto;
  done;

lemma setprod_interval_div: "a <= b ==> (setprod id {1..b}) div (setprod id {1..a}) = (setprod id {Suc a..b})";
  apply (case_tac "b = 0");
  apply (subgoal_tac "a = 0");
  apply (erule ssubst)+;
  apply force+;
  apply (case_tac "a = 0");
  apply (erule ssubst);
  apply force;
  apply (rule sym);
  apply (rule div_multiply);
  apply (case_tac "a = b");
  apply (erule ssubst);
  apply force;
  apply (rule setprod_interval_gt_0);
  apply force+;
  apply (subst nat_mult_commute);
  apply (simp only: setprod_interval_multiply);
  done;

lemma factorial_div: "b <= a ==> (fact a) div (fact b) = setprod id {(Suc b)..a}";
  apply (simp only: factorial_setprod_def setprod_interval_div);
  done;

lemma primes_always_ge_2 [simp]: "p : prime ==> 2 <= p";
  apply (auto simp add: prime_def);
  done;

lemma relprime_dvd_prod_dvd: "gcd(a,b) = 1 ==> a dvd m ==> b dvd m ==> (a*b) dvd (m::nat)";  
  apply (unfold dvd_def);
  apply clarify;
  apply (subgoal_tac "a dvd ka");
  apply (force simp add: dvd_def);
  apply (subst relprime_dvd_mult_iff [THEN sym]);
  apply assumption;
  apply (auto simp add: mult_commute dvd_def);
  apply (rule exI);
  apply (erule sym);
  done;

lemma distinct_primes_gcd_1: "p : prime ==> q : prime ==> p ~= q ==> gcd(p,q) = 1";
  apply (rule prime_imp_relprime);
  apply (auto simp add: prime_def);
  done;

lemma all_relprime_prod_relprime_nat: "finite A ==> ALL x:A. gcd(x,y) = 1 ==> gcd(setprod id A, y) = 1";
  apply (induct set: Finites);
  apply (auto simp add: gcd_mult_cancel);
  done;

lemma prime_product_dvd: "finite A ==> ALL x:A. (x : prime & x dvd M) ==> setprod id A dvd M";
  apply (induct set: Finites);
  apply auto;
  apply (rule relprime_dvd_prod_dvd);
  apply (subst gcd_commute);
  apply (rule all_relprime_prod_relprime_nat);
  apply assumption;
  apply (rule ballI);
  apply (rule distinct_primes_gcd_1);
  apply auto;
  done;
  
lemma pi_setsum_def: "pi (x) = real (setsum (%x. (1::nat)) {y::nat. y <= x & y : prime})";
  proof-;
    have "pi (x) = real(card {y::nat. y <= x & y : prime})";
      by (auto simp add: pi_def);
    also have "... = real(setsum (%x. (1::nat)) {y::nat. y <= x & y : prime})";
      apply (subst real_of_nat_inject);
      apply (rule card_eq_setsum);
      apply (rule finite_subset [of _ "{0..x}"]);
      apply auto;
      done;
    finally show ?thesis;.;
    qed;

lemma set_difference: "{x::nat. x <= y & P(x)} - {x::nat. x <= z & P(x)} = {x::nat. z < x & x <= y & P(x)}";
  by auto;

lemma pi_mono: "y <= x ==> pi(y) <= pi(x)";
  apply (auto simp add: pi_def);
  apply (rule card_mono);
  apply (rule finite_subset [of _ "{0..x}"]);
  apply force+;
  done;

lemma finite_simp [simp]: "finite {z::nat. z <= x & P(x)}";
  apply (rule finite_subset [of _ "{0..x}"]);
  apply force+;
  done;

lemma pi_diff: "y <= x ==> pi(x) - pi(y) = real (setsum (%x. (1::nat)) {z::nat. y < z & z <= x & z : prime})";
  proof-;
    assume "y <= x";
    have mono: "pi (y) <= pi(x)";
      by (insert prems, erule pi_mono);
    have "pi(x) - pi(y) = real(card {z::nat. z <= x & z : prime}) - real(card {z::nat. z <= y & z : prime})";
      by (simp add: pi_def);
    also have "... = real(card {z::nat. z <= x & z : prime} - card {z::nat. z <= y & z : prime})";
      apply (rule real_of_nat_diff [THEN sym]);
      apply (rule card_mono);
      apply (rule finite_subset [of _ "{0..x}"]);
      apply (insert prems, auto);
      done;
    also have "... = real(card {z::nat. y < z & z <= x & z : prime})";
      apply (subst real_of_nat_inject);
      apply (subst card_Diff_subset);
      apply (rule finite_subset [of _ "{0..x}"]);
      apply force+;
      apply auto;
      apply (insert prems, force);
      apply (subst set_difference);
      apply auto;
      done;
    finally show ?thesis;
      apply (subst card_eq_setsum [THEN sym]);
      apply (rule finite_subset [of _ "{0..x}"]);
      apply force+;
      done;
    qed;

lemma pi_less [simp]: "pi(x) <= real x";
  apply (auto simp add: pi_def);
  apply (subgoal_tac "x = card {1..x}");
  apply (erule ssubst);
  apply (rule card_mono);
  apply force+;
  apply auto;
  apply (subgoal_tac "2 <= xa");
  apply arith;
  apply simp;
  done;

lemma mono_setsum_le: "finite A ==> ALL x:A. f x <= (y::'a::ordered_semiring) ==> setsum f A <= setsum (%x. y) A";
  apply (induct set: Finites);
  apply auto;
  apply (rule add_mono);
  apply force+;
  done;
  
lemma setsum_real: "finite A ==> real (setsum (f::nat => nat) (A::nat set)) = setsum (real o f) A";
  apply (induct set: Finites);
  apply auto;
  done;

lemma primes_always_ge_1 [simp]: "p : prime ==> 1 <= p";
  apply (frule primes_always_ge_2);
  apply arith;
  done;
  
lemma powr_divide_denom: "x powr a / x powr b = 1 / (x powr (b - a))";
  apply (simp add: powr_divide2);
  apply (subst powr_minus_divide [THEN sym]);
  apply simp;
  done;
  
lemma setprod_pos: "finite A ==> ALL x:A. ((0::'a::ordered_semiring) < x) ==> 0 < setprod id A";
  apply (induct set: Finites);
  apply force;
  apply (simp add: setprod_insert);
  apply clarify;
  apply (simp add: mult_pos);
  done;

lemma setsum_setprod_ln: "finite A ==> ALL x:A. (0 < x) ==> setsum ln A = ln (setprod id A)";
  apply (induct set: Finites);
  apply force;
  apply (simp add: setsum_insert);
  apply (subgoal_tac "0 < setprod id F");
  apply (simp add: ln_mult);
  apply (rule setprod_pos);
  apply auto;
  done;

lemma setsum_setprod_ln_real: "finite A ==> ALL x:A. ((0::nat) < x) ==> setsum (ln o real) A = ln(real(setprod id A))";
  apply (induct set: Finites);
  apply force;
  apply auto;
  apply (subgoal_tac "0 < real(setprod id F)");
  apply (subgoal_tac "0 < real x");
  apply (simp add: ln_mult);
  apply force;
  apply (subgoal_tac "0 < setprod id F");
  apply force;
  apply (rule setprod_pos);
  apply auto;
  done;

lemma theta_setsum_pos_def: "theta x = setsum lprime {2::nat..x}";
  proof-;
    have step1: "theta x = setsum lprime {0::nat..x}";
      by (simp add: theta_setsum_eq1);
    also have "... = setsum lprime ({0::nat} Un {1::nat..x})";
      apply (rule setsum_cong);
      apply force+;
      done;
    also have "... = setsum lprime {0::nat} + setsum lprime {1::nat..x}";
      apply force;
      done;
    also have "... = setsum lprime {1::nat..x}"
      apply auto;
      apply (auto simp add: lprime_def);
      apply (frule primes_always_ge_2);
      apply force;
      done;
    also have "... = setsum lprime ({1::nat} Un {2::nat..x})";
      apply (case_tac "x = 0");
      apply (simp add: lprime_def);
      apply (rule setsum_cong);
      apply auto;
      done;
    finally show ?thesis;
      apply (auto simp add: lprime_def primes_always_ge_2);
      done;
    qed;

lemma theta_def_2: "theta x = ln (real (setprod id {p. p:prime & p <= x}))";
  apply (subst l.sum_over_F2 [THEN sym]);
  apply (subgoal_tac "finite {p. p:prime & p <= x}");
  apply (subgoal_tac "ALL x:{p. p:prime & p <= x}. (0 < x)");
  apply (simp only: setsum_setprod_ln_real [THEN sym]);
  apply (rule setsum_cong);
  apply auto;
  apply (subgoal_tac "2 <= xa");
  apply (arith);
  apply (simp add: primes_always_ge_2);
  apply (rule finite_subset [of _ "{0..x}"]);
  apply auto;
  done;

lemma lprime_lt_ln: "finite A ==> 0 ~: A ==> setsum lprime A <= setsum (ln o real) A";
  apply (rule setsum_le_cong);
  apply (auto simp add: lprime_def);
  apply (subgoal_tac "1 <= x");
  apply (subgoal_tac "1 <= real(x)");
  apply (simp add: ln_ge_zero);
  apply force+;
  apply (subgoal_tac "x ~= 0");
  apply force+;
  apply (case_tac "x = 0");
  apply force;
  apply force;
  done;

lemma setprod_gt_0_iff: "finite B ==> ((0::nat) < setprod id B) = (0 ~: B)";
  apply auto;
  apply (subgoal_tac "setprod id B = 0");
  apply force;
  apply (subgoal_tac "B = insert 0 (B - {0})");
  apply (erule ssubst);
  apply (subst setprod_insert);
  apply force+;
  apply (induct set: Finites);
  apply force;
  apply auto;
  done;

lemma setsum_subset: "finite B ==> A <= B ==> ALL x:B. 0 <= f x ==> ((setsum f A)::'a::ordered_semiring) <= setsum f B";
  proof-;
    assume "finite B" and "A <= B" and "ALL x:B. 0 <= f x";
    have "setsum f A = setsum f A + 0";
      apply auto;
      done;
    also have "...<= setsum f A + setsum f (B - A)";
      apply (simp only: add_le_cancel_left);
      apply (rule setsum_nonneg);
      apply (insert prems, auto);
      done;
    also have "... = setsum f (A Un (B - A))";
      apply (rule setsum_Un_disjoint [THEN sym]);
      apply (insert prems, auto);
      apply (auto simp add: finite_subset);
      done;
    also have "... = setsum f B";
      apply (insert prems, auto);
      apply (rule setsum_cong);
      apply auto;
      done;
    finally show ?thesis;.;
    qed;

lemma setprod_lt [rule_format]: "finite B ==> 0 ~: B  ==> 
         ALL A. (A <= B -->((setprod id A)::nat) <= setprod id B)";
  proof (clarify);
    assume "finite B" and "0 ~: B";
    fix A;
    assume "A <= B";
    show "setprod id A <= setprod id B";
      proof-;
    have "setprod id B = setprod id (A Un (B - A))";
      apply (rule setprod_cong);
      apply (insert prems);
      apply force+;
      done;
    also have "... = (setprod id A) * (setprod id (B - A))";
      apply (rule setprod_Un_disjoint);
      apply (insert prems, auto);
      apply (auto simp add: finite_subset);
      done;
    also have "setprod id A <= ...";
      apply auto;
      apply (rule Suc_leI);
      apply (subst setprod_gt_0_iff);
      apply (insert prems, auto simp add: finite_subset);
      done;
    finally; show ?thesis;.;
    qed;
    qed;

lemma lt_one_minus: "x <= n ==> x ~= n ==> x <= (n - Suc 0)";
  apply (subst Suc_le_mono [THEN sym]);
  apply simp;
  done;

lemma only_even_prime: "p : prime ==> even p ==> p = 2";
  apply (case_tac "p = 2");
  apply force;
  apply (simp add: even_mult_two_ex);
  apply (erule exE);
  apply (auto simp add: prime_def);
  done;

lemma dvd_div: "a : prime ==> a dvd b ==> ~(a dvd c) ==> b mod c = 0  ==> a dvd (b div c)";
  apply auto;
  apply (frule prime_dvd_mult);
  apply auto;
  done;

(* Simple Facts About Binomial Coefficients *)

subsection {* Binomial coefficients -- break this out! *}

lemma binomial_factorial_def_lemma1: "fact (Suc y) * fact(Suc x - Suc y) * (x choose y) = (Suc y) * fact y * fact(x-y)*(x choose y)";
  apply simp;
done;

lemma binomial_factorial_def_lemma2: "fact (Suc y) * fact(Suc x - Suc y) * (x choose Suc y) = (x-y)*fact (Suc y) * fact(x - Suc y) * (x choose Suc y)";
  apply simp;
  apply (case_tac "x <= y");
  apply auto;
  apply (simp add: binomial_eq_0_iff);
  apply (case_tac "x = Suc y");
  apply force;
  apply (subgoal_tac "y < x");
  apply auto;
  apply (subgoal_tac "x-y = Suc (x - Suc y)");
  apply (erule ssubst);
  apply force;
  apply arith;
  done;

lemma binomial_factorial_def [rule_format]: "ALL n k.  k<=n --> fact(k) * fact(n-k) * (n choose k) = fact(n)";
  apply (rule allI);
  apply (induct_tac n);
  apply force;
  apply auto;
  apply (case_tac k);
  apply (erule ssubst);
  apply force;
  apply (subgoal_tac "Suc nat <= Suc na");
  apply (erule ssubst);
  apply (simp only: binomial_Suc_Suc);
  apply (simp only: ring_distrib);
  apply (simp only: binomial_factorial_def_lemma1 binomial_factorial_def_lemma2);
  apply (case_tac "Suc nat = Suc na");
  apply force;
  apply (subgoal_tac "Suc nat <= na");
  apply (frule_tac x = "Suc nat" in spec);
  apply (frule_tac x = "nat" in spec);
  apply (subgoal_tac "nat <= na");
  apply (drule mp);
  apply force;
  apply (drule mp);
  apply force;
  apply (subgoal_tac "Suc nat * fact nat * fact (na - nat) * (na choose nat) = Suc nat * (fact nat * fact (na - nat) * (na choose nat))");
  apply (erule ssubst);
back;
back;
  apply (erule ssubst);
back;
  apply (subgoal_tac "(na - nat) * fact (Suc nat) * fact (na - Suc nat) * (na choose Suc nat) = (na - nat) * (fact (Suc nat) * fact (na - Suc nat) * (na choose Suc nat))");
  apply (erule ssubst);
back;
  apply (erule ssubst);
  apply (simp add: ring_distrib [THEN sym]);
  apply force;
  apply (simp only: nat_mult_assoc);
  apply auto;
done;

(* Division with the natural numbers is unwieldy, so make sure to have lemmas like the following two when dealing with binomial coefficients, whose definition does deal with division with the natural numbers. *)

lemma binomial_mod: "k <= n ==> fact(n) mod (fact(k) * fact(n-k)) = 0";
  apply (simp add: mod_eq_0_iff);
  apply (rule_tac x = "n choose k" in exI);
  apply (simp add: binomial_factorial_def);
done;

lemma binomial_dvd: "k <= n ==> (fact(k) * fact(n-k)) dvd fact(n)";
  apply (simp add: binomial_mod dvd_eq_mod_eq_0);
done;

lemma binomial_factorial_def_div: "k <= n ==> n choose k = fact(n) div (fact(k) * fact (n-k))";
  apply (frule binomial_dvd);
  apply (drule dvd_mult_div_cancel);
  apply (frule binomial_factorial_def);
  apply (rule product_div);
  apply (rule mult_pos);
  apply auto;
  apply (auto simp add: mult_commute);
  done;

lemma binomial_step: "1 <= k ==> k <= n ==> k * (n choose k) = (n - (k - 1))*(n choose (k - 1))";
  apply (subgoal_tac "k - 1 <= n");
  apply (simp only: binomial_factorial_def_div);
  apply (frule binomial_mod [of "k" "n"]);
  apply (frule binomial_mod [of "k - 1" "n"]);
  apply (simp only: div_combine);
  apply (simp only: factorial_pos [of k]);
  apply (subgoal_tac "1 <= n - (k - 1)");
  apply (simp only: factorial_pos [of "n - (k - 1)"]);
  apply (subgoal_tac "0 < k");
  apply (subgoal_tac "0 < (n - (k - 1))");
  apply (subgoal_tac "(fact (k - (1::nat)) * ((n - (k - (1::nat))) * fact (n - (k - (1::nat)) - (1::nat)))) = ((n - (k - 1)) * (fact (k - (1::nat)) * fact (n - (k - (1::nat)) - (1::nat))))");
  apply (erule ssubst);
back;
back;
  apply (simp add: div_mult_mult1 [of "k" _ _] div_mult_mult1 [of "(n - (k - 1))" _ _]);
  apply force;
  apply force;
  apply force;
  apply simp;
  apply (subgoal_tac "0 <= n-k");
  apply (simp add: Suc_le_mono Suc_diff_le);
  apply force;
  apply (rule Suc_leD);
  apply (subgoal_tac "(1::nat) = Suc 0");
  apply (erule ssubst);
  apply (subgoal_tac "0 < k");
  apply (simp add: Suc_pred);
  apply auto;
done;

lemma binomial_n_n: "n choose n = 1";
  apply (simp add: binomial_factorial_def);
done;

lemma binomial_n_0: "n choose 0 = 1";
  apply (simp add: binomial_0);
done;

lemma binomial_sym: "k <= n ==> n choose k = n choose (n-k)";
  apply (simp add: binomial_factorial_def_div);
  apply (subgoal_tac "n - (n - k) = k");
  apply (erule ssubst);
  apply (subgoal_tac "fact k * fact(n-k) = fact(n-k) * fact k");
  apply (erule ssubst);
  apply auto;
done;

lemma binomial_minus: "Suc k <= n ==> fact(n-k) = (n-k) * fact(n - Suc k)";
  apply (subgoal_tac "n-k = Suc (n - Suc k)");
  apply (erule ssubst);
  apply (simp only: fact_Suc);
  apply (simp add: Suc_diff_le [THEN sym]);
done;

lemma divide_mod_equality: "a mod b = (0::nat) ==> (a div b) * b = a";
  apply auto;
done;

lemma binomial_def: "k<=n ==> 0 < k ==> (n choose k) + (n choose (k - Suc 0)) = (Suc n choose k)";
  apply (simp add: binomial_Suc);
done;

lemma binomial_0: "n choose Suc n = 0";
  apply (simp add: binomial_eq_0_iff);
done;

lemma binomial_gt_0 [simp]: "k <= n ==> 0 < n choose k";
  apply (rule contrapos_pp);
  apply auto;
  apply (simp add: binomial_eq_0_iff);
  done;

(* x and y are casted to nats because of the multiplication at the right - probably easily generalized *)
lemma binomial_theorem: "(x+y)^n = setsum (%i. (n choose i)*x^i*y^(n-i)) {0..n}";
  apply (induct_tac n);
  apply force;
  apply (simp add: power_Suc);
  apply (simp add: add_mult_distrib);
  apply (simp add: setsum_multiplier);
  apply (subgoal_tac "(∑i::nat:{0::nat..n}. x * ((n choose i) * x ^ i * y ^ (n - i))) = (∑i::nat:{0::nat..n}. ((n choose i) * x ^ Suc i * y ^ (n - i)))");
  apply (erule ssubst);
  apply (erule ssubst);
  apply (subgoal_tac "(∑i::nat:{0::nat..n}. y * ((n choose i) * x ^ i * y ^ (n - i))) = (∑i::nat:{0::nat..n}. ((n choose i) * x ^ i * y ^ (Suc n - i)))");
  apply (erule ssubst);
  apply (subgoal_tac "(∑i::nat:{0::nat..n}. (n choose i) * x ^ Suc i * y ^ (n - i)) = (∑i::nat:{1::nat..(n+1)}. (n choose (i-(1::nat))) * x ^ ((Suc i) - (1::nat)) * y ^ (Suc n - i))");
  apply (erule ssubst);
  apply (subgoal_tac "(∑i::nat:{0::nat..n}. (n choose i) * x ^ i * y ^ (Suc n - i)) = ((n choose 0)*x^0*y^Suc n) + (∑i::nat:{1::nat..n+1}. (n choose i) * x ^ i * y ^ (Suc n - i))");
  apply (erule ssubst);
  apply (simp only:plus_ac0);
  apply (simp add: setsum_addf [THEN sym]);
  apply (simp add: add_mult_distrib [THEN sym]);
  apply (subgoal_tac "(∑xa::nat:{Suc (0::nat)..Suc n}. (n choose xa + (n choose (xa - Suc (0::nat)))) * x ^ xa * y ^ (Suc n - xa)) = (∑xa::nat:{Suc (0::nat)..Suc n}. (Suc n choose xa) * x ^ xa * y ^ (Suc n - xa))");
  apply (erule ssubst);
  apply (subgoal_tac "y * y^n = (Suc n choose 0) * x^0 * y^(Suc n - 0)");
  apply (erule ssubst);
  apply (subgoal_tac "0 ~: {Suc 0..Suc n}");
  apply (subgoal_tac "finite {Suc 0..Suc n}");
  apply (subgoal_tac "{0..Suc n} = insert 0 {Suc 0..Suc n}");
  apply (erule ssubst);
  apply (subgoal_tac "(∑i::nat:insert (0::nat) {Suc (0::nat)..Suc n}. (Suc n choose i) * x ^ i * y ^ (Suc n - i)) = (Suc n choose 0) * x ^ 0 * y ^ (Suc n - 0) + (∑i::nat:{Suc (0::nat)..Suc n}. (Suc n choose i) * x ^ i * y ^ (Suc n - i))");
  apply (erule ssubst);
  apply force;
  apply (simp add: setsum_insert);
  apply force;
  apply force;
  apply force;
  apply force;
  apply (rule setsum_cong);
  apply force;
  apply (case_tac "xa = Suc n");
  apply (erule ssubst);
  apply (simp add: binomial_0);
  apply (subgoal_tac "xa <= n");
  apply (subgoal_tac "0 < xa");
  apply (simp add: binomial_def);
  apply force;
  apply force;
  apply (subgoal_tac "y ^ Suc n = y ^ (Suc n - 0)");
  apply (erule ssubst);
  apply (subgoal_tac "0 ~: {1::nat..n+1}");
  apply (subgoal_tac "finite {1::nat..n+1}");
  apply (subgoal_tac "(n choose (0::nat)) * x ^ (0::nat) * y ^ (Suc n - (0::nat)) + (∑i::nat:{1::nat..n + (1::nat)}. (n choose i) * x ^ i * y ^ (Suc n - i)) = (∑i::nat:{0::nat..n + (1::nat)}. (n choose i) * x ^ i * y ^ (Suc n - i))");
  apply (erule ssubst);
  apply (subgoal_tac "{0::nat..n+1} = insert (n+1) {0..n}");
  apply (erule ssubst);
  apply (subgoal_tac "(n+1) ~: {0::nat..n}");
  apply (subgoal_tac "finite {0::nat..n}");
  apply (simp add: setsum_insert);
  apply (simp add: binomial_0);
  apply force;
  apply force;
  apply force;
  apply (subgoal_tac "{0::nat..n + (1::nat)} = insert 0 {1::nat..n+1}");
  apply (erule ssubst);
  apply (simp add: setsum_insert);
  apply force;
  apply force;
  apply force;
  apply force;
  apply (subgoal_tac "(∑i::nat:{1::nat..n + (1::nat)}. (n choose (i - (1::nat))) * x ^ (Suc i - (1::nat)) * y ^ (Suc n - i)) = (∑i::nat:{1::nat..n + (1::nat)}. (n choose (i - (1::nat))) * x ^ (Suc (i - 1::nat)) * y ^ (n - (i-(1::nat))))");
  apply (erule ssubst);
  apply (rule setsum_index_shift_right);
  apply (rule setsum_cong);
  apply force;
  apply (subgoal_tac "Suc xa - 1 = xa");
  apply (erule ssubst);
  apply (subgoal_tac "Suc (xa - (1::nat)) = xa");
  apply (erule ssubst);
  apply (subgoal_tac "Suc n - xa = n - (xa - (1::nat))");
  apply (erule ssubst);
  apply simp;
  apply simp;
  apply simp;
  apply (rule Suc_pred);
  apply force;
  apply force;
  apply (rule setsum_cong);
  apply force;
  apply simp;
  apply (simp only: power_Suc [THEN sym]);
  apply (simp add: Suc_diff_le);
  apply (rule setsum_cong);
  apply force;
  apply simp;
done;

subsection {* Beginning of Chebyshev's theorem *}

(* Now begins the proof of Lemma 8.1, on unimodality. We will first prove some basic lemmas involving 
   products and inequalities *)

lemma binomial_unimodal_1: "1 <= n ==> 1 <= k ==> k <= n ==> (n choose (k - 1) < n choose k) = (2*k < n+1)"; 
  proof-;
    assume npos: "1 <= n";
    assume kpos: "1 <= k";
    assume kn: "k <= n";
    have step1: "k * (n choose k) = (n - (k - 1))*(n choose (k - 1))";
      apply (rule binomial_step);
      apply (auto simp only: kpos kn);
      done;
    have a0: "0 < k";
      apply (subgoal_tac "1 <= k");
      apply force;
      apply (simp only: kpos);
      done;
    have a1: "0 < (n choose k)";
      apply (case_tac "n choose k");
      apply (simp add: binomial_eq_0_iff);
      apply auto;
      apply (subgoal_tac "k <= n");
      apply force;
      apply (simp add: kn);
      done;
    have a2: "0 < n - (k - 1)";
      apply auto;
      apply (rule Suc_le_lessD);
      apply (subgoal_tac "0 < k");
      apply (simp add: Suc_pred);
      apply (auto simp add: kn a0);
      done;
    have a3: "0 < (n choose (k - 1))";
      apply (case_tac "n choose (k - 1)");
      apply (simp add: binomial_eq_0_iff);
      apply auto;
      apply (subgoal_tac "k <= n");
      apply (simp only: Suc_less_eq [of "n" "k - Suc (0::nat)", THEN sym]);
      apply (subgoal_tac "0 < k");
      apply (simp add: Suc_pred);
      apply (simp add: a0);
      apply (simp add: kn);
      done;
    from step1 a0 a1 a2 a3 show ?thesis;
      apply (simp only: gt_lt_product_iff [of "k" "n choose k" "n - (k - 1)" "n choose (k - 1)"]);
      apply simp;
      apply (simp add: nat_less_diff [of "k" "Suc n" "k"]);
      apply auto;
      done;
    qed;

lemma binomial_unimodal_Suc_1: "1 <= n ==> k < n ==> (n choose k) < (n choose Suc k) = (2 * Suc k < n+1)";
  apply (subgoal_tac "1 <= Suc k");
  apply (subgoal_tac "Suc k <= n");
  apply (subgoal_tac "n choose k = n choose (Suc k - 1)");
  apply (erule ssubst);
  apply (simp only: binomial_unimodal_1 [of "n" "Suc k"]);
  apply auto;
done;

lemma binomial_unimodal_2: "1 <= n ==> 1 <= k ==> k <= n ==> (n choose k < n choose (k - 1)) = (n+1 < 2*k)";
  proof-;
    assume n: "1 <= n";
    assume k: "1 <= k";
    assume kn: "k <= n";
    have step1: "(n - (k - 1))*(n choose (k - 1)) = k * (n choose k)";
      apply (simp only: eq_sym_conv);
      apply (rule binomial_step);
      apply (auto simp only: k kn);
      done;
    have a0: "0 < k";
      apply (subgoal_tac "1 <= k");
      apply force;
      apply (simp only: k);
      done;
    have a1: "0 < (n choose k)";
      apply (case_tac "n choose k");
      apply (simp add: binomial_eq_0_iff);
      apply auto;
      apply (subgoal_tac "k <= n");
      apply force;
      apply (simp add: kn);
      done;
    have a2: "0 < n - (k - 1)";
      apply auto;
      apply (rule Suc_le_lessD);
      apply (subgoal_tac "0 < k");
      apply (simp add: Suc_pred);
      apply (auto simp add: kn a0);
      done;
    have a3: "0 < (n choose (k - 1))";
      apply (case_tac "n choose (k - 1)");
      apply (simp add: binomial_eq_0_iff);
      apply auto;
      apply (subgoal_tac "k <= n");
      apply (simp only: Suc_less_eq [of "n" "k - Suc (0::nat)", THEN sym]);
      apply (subgoal_tac "0 < k");
      apply (simp add: Suc_pred);
      apply (simp add: a0);
      apply (simp add: kn);
      done;
    from step1 a0 a1 a2 a3 show ?thesis;
      apply (simp only: gt_lt_product_iff [of "n - (k - 1)" "n choose (k - 1)" "k" "n choose k"]);
      apply simp;
      apply (subgoal_tac "(Suc n - k < k) = (k + (Suc n - k) < k + k)");
      apply (erule ssubst);back;
      apply force;
      apply (simp only: nat_add_left_cancel_less [THEN sym]);
      done;
    qed;

lemma binomial_unimodal_Suc_2: "1 <= n ==> k < n ==> (n choose Suc k) < (n choose k) = (n+1 < 2 * Suc k)";
  apply (subgoal_tac "1 <= Suc k");
  apply (subgoal_tac "Suc k <= n");
  apply (subgoal_tac "n choose k = n choose (Suc k - 1)");
  apply (erule ssubst);
  apply (simp only: binomial_unimodal_2 [of "n" "Suc k"]);
  apply auto;
done;

lemma binomial_unimodal_3: "1 <= n ==> 1 <= k ==> k <= n ==> (n choose k = n choose (k - 1)) = (2*k = n+1)";
  proof-;
    assume n: "1 <= n";
    assume k: "1 <= k";
    assume kn: "k <= n";
    have step1: "(n - (k - 1))*(n choose (k - 1)) = k * (n choose k)";
      apply (simp only: eq_sym_conv);
      apply (rule binomial_step);
      apply (auto simp only: k kn);
      done;
    have a0: "0 < k";
      apply (subgoal_tac "1 <= k");
      apply force;
      apply (simp only: k);
      done;
    have a1: "0 < (n choose k)";
      apply (case_tac "n choose k");
      apply (simp add: binomial_eq_0_iff);
      apply auto;
      apply (subgoal_tac "k <= n");
      apply force;
      apply (simp add: kn);
      done;
    have a2: "0 < n - (k - 1)";
      apply auto;
      apply (rule Suc_le_lessD);
      apply (subgoal_tac "0 < k");
      apply (simp add: Suc_pred);
      apply (auto simp add: kn a0);
      done;
    have a3: "0 < (n choose (k - 1))";
      apply (case_tac "n choose (k - 1)");
      apply (simp add: binomial_eq_0_iff);
      apply auto;
      apply (subgoal_tac "k <= n");
      apply (simp only: Suc_less_eq [of "n" "k - Suc (0::nat)", THEN sym]);
      apply (subgoal_tac "0 < k");
      apply (simp add: Suc_pred);
      apply (simp add: a0);
      apply (simp add: kn);
      done;
    from step1 a0 a1 a2 a3 show ?thesis;
      apply (simp only: eq_product_iff [of "n - (k - 1)" "n choose (k - 1)" "k" "n choose k"]);
      apply simp;
      apply (subst eq_sym_conv [of "Suc n - k" "k"]);
      apply (simp only: nat_add_right_cancel [of "k" "k" "Suc n - k", THEN sym]);
      apply auto;
      done;
    qed;

lemma binomial_unimodal_Suc_3: "1 <= n ==> k < n ==> (n choose Suc k) = (n choose k) = (2 * Suc k = n+1)";
  apply (subgoal_tac "1 <= Suc k");
  apply (subgoal_tac "Suc k <= n");
  apply (subgoal_tac "n choose k = n choose (Suc k - 1)");
  apply (erule ssubst);
  apply (simp only: binomial_unimodal_3 [of "n" "Suc k"]);
  apply auto;
done;

(* Now we are going to prove Lemma 8.2. First, we need preliminaries . . . *)

lemma binomial_two_level_equality: "1 <= n ==> (2*n + 2) choose (n+1) = (2*n choose (n - 1)) + 2*(2*n choose n) + (2*n choose (n+1))";
  apply (simp add: binomial_Suc);
done;

lemma binomial_two_level_inequality: "1 <= n ==> 2*(2*n choose n) <= (2*n+2) choose (n+1)";
  apply (subgoal_tac "(2*n + 2) choose (n+1) = (2*n choose (n - 1)) + 2*(2*n choose n) + (2*n choose (n+1))");
  apply force;
  apply (simp only: binomial_two_level_equality);
done;

lemma binomial_two_level_inequality_Suc: "1 <= n ==> 2*(2*n choose n) <= (2*Suc n choose Suc n)";
  apply (subgoal_tac "2*Suc n = 2*n+2");
  apply (erule ssubst);
  apply (subgoal_tac "Suc n = n+1");
  apply (erule ssubst);
  apply (simp only: binomial_two_level_inequality);
  apply auto;
done;

lemma binomial_always_ge_2 [rule_format]: "0 < n --> 2 <= (2*n choose n)";
  apply (induct_tac n);
  apply auto;
  apply (simp add: binomial_Suc_Suc);
done;

lemma extended_unimodality_lemma: "1 <= n ==> ALL i < n. (2*n choose i) < (2*n choose Suc i)";
  apply auto;
  apply (subgoal_tac "2*Suc i < 2*n+1");
  apply (simp add: binomial_unimodal_Suc_1);
  apply auto;
done;

lemma extended_unimodality_1: "1 <= n ==> k < n ==> (2*n choose k) < (2*n choose n)";
  apply (rule chained_inequalities_up [of "n" "(%i. (2*n choose i))" "k"]);
  apply (simp add: extended_unimodality_lemma);
  by auto;

lemma extended_unimodality_lemma_2: "1 <= n ==> ALL i < 2*n. (n <= i --> (2*n choose Suc i) < (2*n choose i))";
  apply auto;
  apply (subgoal_tac "2*n + 1 < 2 * Suc i");
  apply (simp add: binomial_unimodal_Suc_2);
  apply force;
done;

lemma extended_unimodality_2: "1 <= n ==> n < k  ==> (2*n choose k) < (2*n choose n)";
  apply (case_tac "k <= 2*n");
  apply (frule less_imp_Suc_add);
  apply auto;
  apply (simp only: add_Suc_right [THEN sym]);
  apply (subgoal_tac "2*n choose (n + Suc k) = 2*n choose (n - Suc k)");
  apply (erule ssubst);
  apply (subgoal_tac "(n - Suc k) < n");
  apply (simp add: extended_unimodality_1);
  apply force;
  apply (simp add: binomial_sym);
  apply (subgoal_tac "2*n choose k = 0");
  apply (erule ssubst);
  apply (subgoal_tac "2 <= 2*n choose n");
  apply force;
  apply (auto simp add: binomial_always_ge_2 binomial_eq_0_iff);
done;

lemma middle_binomial_is_max: "k <= 2*n ==> (2*n choose k) <= (2*n choose n)";
  apply (case_tac "n = 0");
  apply force;
  apply (subgoal_tac "1 <= n");
  apply (case_tac "k < n");
  apply (frule extended_unimodality_1);
  apply force+;
  apply (case_tac "k = n");
  apply force+;
  apply (subgoal_tac "n < k");
  apply (frule extended_unimodality_2);
  apply force+;
done;

lemma binomial_theorem_for_2: "(1+1)^n = setsum (%i. (n choose i)) {0..n}";
  apply (simp only: binomial_theorem);
  apply (auto simp only: power_one);
  apply simp;
done;

lemma middle_binomial_bound_high: "0 < n ==> (2*n choose n) < 2^(2*n)";
  proof-;
    assume pos: "0 < n";
    have step1: "(2*n choose n) < setsum (%i. 2*n choose i) {0..2*n}";
      apply (rule sum_greater_than_part);
      apply force+;
      apply (subgoal_tac "2*n : {0..2*n}");
      apply (subgoal_tac "2*n ~= n");
      apply force;
      apply (auto simp add: pos);
      done;
    also; have "... = (1+1)^(2*n)";
      apply (simp only: binomial_theorem_for_2);
      done;
    also have "... = 2^(2*n)";
      apply (subgoal_tac "1+1 = 2");
      apply (erule ssubst);
      apply force;
      apply force;
      done;
    finally show ?thesis;.;
    qed;

lemma middle_binomial_bound_low: "1 <= n ==> 2^(2*n) <= 2*n*(2*n choose n)";
  proof-;
    assume pos: "1 <= n";
    have "(2::nat)^(2*n) = (1+1)^(2*n)";
      apply (subgoal_tac "1+1 = 2");
      apply (erule ssubst);
      apply auto;
      done;
    also have "... = setsum (%i. 2*n choose i) {0..2*n}";
      apply (rule binomial_theorem_for_2);
      done;
    also have "... = 1 + setsum (%i. 2*n choose i) {1..2*n}";
      apply (subgoal_tac "{0..2*n} = insert 0 {1..2*n}");
      apply (simp add: setsum_insert);
      apply force;
      done;
    also have "... = 1 + 1 + setsum (%i. 2*n choose i) {1..(2*n - 1)}";
      apply (subgoal_tac "{1..2*n} = insert (2*n) {1..(2*n - 1)}");
      apply (erule ssubst);
      apply (subgoal_tac "finite {1::nat..(2::nat) * n - (1::nat)}");
      apply (subgoal_tac "(2*n) ~: {1..(2*n - 1)}");
      apply (simp add: setsum_insert);
      apply (simp add: pos);
      apply auto;
      apply (simp add: Suc_le_mono [of "2*n" "2*n - Suc 0", THEN sym]);
      apply (simp add: not_le_iff_less);
      apply (subgoal_tac "Suc (2*n - Suc 0) < Suc x");
      apply (simp only: Suc_pred);
      apply (simp only: Suc_less_eq);
      apply (subgoal_tac "1 <= n");
      apply force;
      apply (simp only: pos);
      apply (subgoal_tac "Suc x <= Suc (2*n - Suc 0)");
      apply (subgoal_tac "0 < 2*n");
      apply (simp add: Suc_pred);
      apply (simp add: pos);
      apply (subgoal_tac "1 <= n");
      apply force;
      apply (rule pos);
      apply simp;
      done;
    also have "... = 2 + setsum (%i. 2*n choose i) {1..(2*n - 1)}";
      by auto;
    also have "... <= 2 + (2*n - 1)*(2*n choose n)";
       apply simp;
       apply (subgoal_tac "((2::nat) * n - Suc (0::nat))*(2*n choose n) = card({Suc (0::nat)..(2::nat) * n - Suc (0::nat)}) *(2*n choose n)");
       apply (erule ssubst);
       apply (rule setsum_constant_bound [of "{Suc (0::nat)..(2::nat) * n - Suc (0::nat)}" "(%i. 2*n choose i)" "2*n choose n"]);
       apply force;
       apply (auto simp add: middle_binomial_is_max);
       apply (subgoal_tac "x <= 2*n");
       apply (auto simp add: middle_binomial_is_max);
       apply (rule nat_le_diff);
       apply force;
       done;
     also have "... <= (2*n choose n) + (2*n - 1)*(2*n choose n)";
       apply (auto);
       apply (rule binomial_always_ge_2);
       apply (subgoal_tac "1 <= n");
       apply force;
       apply (intro pos);
       done;
     also have "... = 1*(2*n choose n) + (2*n - 1) * (2*n choose n)";
       apply auto;
       done;
     also have "... = (2*n)*(2*n choose n)";
       apply (simp only: add_mult_distrib [THEN sym]);
       apply (subgoal_tac "1 + (2*n - 1) = 2*n");
       apply (erule ssubst);
       apply simp;
       apply (rule le_add_diff_inverse);
       apply (subgoal_tac "1 <= n");
       apply force;
       apply (simp only: pos);
       done;
     finally show ?thesis;.;
     qed;

lemma extended_unimodality_lemma_odd: "1 <= n ==> ALL i < n. (Suc(2*n) choose i) < (Suc(2*n) choose Suc i)";
  apply (auto);
  apply (subgoal_tac "2*Suc i < Suc(2*n) + 1");
  apply (simp only: binomial_unimodal_Suc_1 [THEN sym]);
  apply auto;
  done;

lemma extended_unimodality_odd_1: "1 <= n ==> k < n ==> (Suc(2*n) choose k) < (Suc(2*n) choose n)";
  apply (rule chained_inequalities_up [of "n" "(%i. Suc(2*n) choose i)" "k"]);
  apply (simp add: extended_unimodality_lemma_odd);
  apply force;
  done;

lemma extended_unimodality_odd_2: "1 <= n ==> Suc n < k ==> (Suc(2*n) choose k) < (Suc(2*n) choose Suc n)";
  apply (case_tac "Suc(2*n) < k");
  apply (subgoal_tac "Suc(2*n) choose k = 0");
  apply (erule ssubst);
  apply (simp add: binomial_Suc_Suc);
  apply (subgoal_tac "2 <= 2*n choose n");
  apply (simp add: binomial_eq_0_iff);
  apply (simp add: binomial_always_ge_2);
  apply (subgoal_tac "k <= Suc(2*n)");
  apply (subgoal_tac "(Suc(2*n) choose k) = (Suc(2*n) choose (Suc(2*n) - k))");
  apply (erule ssubst);
  apply (subgoal_tac "(Suc(2*n) choose Suc n) = (Suc(2*n) choose n)");
  apply (erule ssubst);
  prefer 4;
  apply force;
  apply (subgoal_tac "(Suc(2*n) - k) < n");
  apply (simp add: extended_unimodality_odd_1);
  apply (simp only: nat_add_left_cancel_less [of "k" "Suc(2*n) - k" "n", THEN sym]);
  apply (simp add: le_add_diff_inverse);
  apply (subgoal_tac "Suc(2*n) choose n = Suc(2*n) choose (Suc(2*n) - Suc n)");
  apply (erule ssubst);
  apply (subst binomial_sym);
  apply force+;
  apply (simp only: binomial_sym);
  done;

lemma middle_binomial_is_max_odd: "1 <= n ==> (Suc(2*n) choose k) <= (Suc(2*n) choose n)"; 
  apply (case_tac "Suc(2*n) < k");
  apply (subgoal_tac "Suc(2*n) choose k = 0");
  apply (subgoal_tac "Suc(2*n) choose n = Suc(2*n) choose Suc n");
  apply (erule ssubst)+;
  apply (simp add: binomial_Suc_Suc);
  apply (subgoal_tac "2 <= 2*n choose n");
  apply (simp only: binomial_sym);
  apply simp;
  apply (simp add: binomial_always_ge_2);
  apply (simp add: binomial_eq_0_iff);
  apply (case_tac "k < n");
  apply (subgoal_tac "Suc ((2::nat) * n) choose k < Suc ((2::nat) * n) choose n");
  apply simp;
  apply (simp add: extended_unimodality_odd_1);
  apply (case_tac "Suc n < k");
  apply (subgoal_tac "Suc (2*n) choose n = Suc (2*n) choose (Suc n)");
  apply (erule ssubst);
  apply (subgoal_tac "Suc ((2::nat) * n) choose k < Suc ((2::nat) * n) choose Suc n");
  apply simp;
  apply (force intro: extended_unimodality_odd_2);
  apply (simp only: binomial_sym, simp);
  apply auto;
  apply (case_tac "k = n");
  apply (erule ssubst);
  apply force;
  apply (case_tac "k = Suc n");
  apply (erule ssubst);
  apply (subgoal_tac "Suc ((2::nat) * n) choose Suc n = Suc ((2::nat) * n) choose n");
  apply force;
  apply (simp only: binomial_sym, simp);
  apply force;
  done;

lemma middle_odd_binomial: "(Suc(2*m) choose m) = (Suc(2*m) choose Suc m)";
  apply (subgoal_tac "Suc(2*m) - m = Suc m");
  apply (simp only: binomial_sym);
  apply auto;
  done;

lemma binomial_sum_lemma_1: "1 <= m ==> 2*(Suc(2*m) choose m) < 2^(Suc(2*m))";
  proof-;
    assume m: "1 <= m";
    have "2*(Suc(2*m) choose m) = (Suc(2*m) choose m) + (Suc(2*m) choose Suc m)";
      apply (auto simp add: middle_odd_binomial);
      done;
    also have "... = setsum (%i. (Suc(2*m) choose i)) {m,Suc m}";
      apply auto;
      done;
    also have "... < setsum (%i. (Suc(2*m) choose i)) {0..Suc(2*m)}";
      apply (rule sum_is_greater_than_part);
      apply force;
      apply force;
      apply clarsimp;
      apply (case_tac "0 = Suc(2*m) choose x");
      apply (simp add: binomial_eq_0_iff);
      apply auto;
      apply (subgoal_tac "0 : {0..Suc(2*m)}");
      apply (subgoal_tac "0 ~: {m,Suc m}");
      apply force;
      apply (simp);
      apply (subgoal_tac "1 <= m");
      apply force;
      apply (simp only: m);
      apply force;
      apply (subgoal_tac "0 : {0..Suc(2*m)}");
      apply (subgoal_tac "0 ~: {m,Suc m}");
      apply force;
      apply simp;
      apply (subgoal_tac "1 <= m");
      apply force;
      apply (simp only: m);
      apply force;
      done;
    also have "... = (1+1)^(Suc(2*m))";
      apply (simp only: binomial_theorem_for_2);
      done;
    also have "... = 2^(Suc(2*m))";
      apply (subgoal_tac "1+1 = (2::nat)");
      apply (erule ssubst);
      apply auto;
      done;
    finally show ?thesis;.;
    qed;

lemma binomial_sum_lemma_2: "1 <= m ==> (Suc(2*m) choose m) < 2^(2*m)";
  proof-;
    assume m: "1 <= m";
    have step1: "2*(Suc(2*m) choose m) < 2^(Suc(2*m))";
      apply (rule binomial_sum_lemma_1);
      apply (rule m);
      done;
    then; have "(Suc(2*m) choose m) < 2^(2*m)";
      apply auto;
      done;
    then show ?thesis;.;
    qed;

lemma binomial_sum_lemma_3: "1 <= m ==> Suc(2*m) choose Suc m < 2^(2*m)";
  apply (subgoal_tac "Suc(2*m) choose Suc m = Suc(2*m) choose m");
  apply (erule ssubst);
  apply (simp only: binomial_sum_lemma_2);
  apply (simp only: middle_odd_binomial);
  done;

lemma binomial_sum_lemma_4: "1 <= m ==> Suc(2*m) choose m < 4^m";
  proof-;
    assume m: "1 <= m";
    have "Suc(2*m) choose m < 2^(2*m)";
      apply (rule binomial_sum_lemma_2);
      apply (rule m);
      done;
    also have "... = 4^m";
      apply (simp add: power_mult);
      done;
    finally show ?thesis;.;
    qed;


lemma binomial_factorial_simplified: "k <= n ==> (n choose k) = setprod id {(Suc k)..n} div setprod id {1..(n-k)}";
  apply (subst binomial_factorial_def_div);
  apply force;
  apply (subst div_mult2_eq);
  apply (subst factorial_div);
  apply force;
  apply (simp only: factorial_setprod_def);
  done;

lemma binomial_odd_def: "1 <= m ==> (Suc(2*m) choose m) = setprod id {m+2..Suc(2*m)} div setprod id {1..m}";
  apply (subgoal_tac "(Suc(2*m) choose m) = (Suc(2*m) choose Suc m)");
  apply (erule ssubst);
  apply (subst binomial_factorial_simplified);
  apply force;
  apply (subgoal_tac "m + 2 = Suc (Suc m)");
  apply (erule ssubst);
  apply (subgoal_tac "Suc(2*m) - Suc m = m");
  apply (erule ssubst);
  apply force+;
  apply (simp only: binomial_sym);
  apply force;
  done;

lemma binomial_setprod_multiply: "k <= n ==> (setprod id {1..k})*(setprod id {1..(n-k)})*(n choose k) = setprod id {1..n}";
  apply (simp only: factorial_setprod_def [THEN sym]);
  apply (simp only: binomial_factorial_def);
  done;

lemma binomial_setprod_multiply_reduced: "k <= n ==> (setprod id {1..(n-k)})*(n choose k) = setprod id {Suc(k)..n}";
  apply (subgoal_tac "setprod id {1..k} * (setprod id {1::nat..n - k} * (n choose k)) = setprod id {1..k} * setprod id {Suc k..n}");
  apply (simp only: mult_cancel1);
  apply (subgoal_tac "0 < setprod id {Suc 0..k}");
  apply simp;
  apply simp;
  apply (subst nat_mult_assoc [THEN sym]);
  apply (simp only: binomial_setprod_multiply);
  apply (simp only: setprod_interval_multiply);
  done;

lemma binomial_setprod_mod [simp]: "setprod id {Suc k..n} mod setprod id {1..(n-k)} = 0";
  apply (case_tac "n < k");
  apply simp;
  apply (subgoal_tac "k <= n");
  apply (simp only: mod_eq_0_iff);
  apply (rule_tac x = "(n choose k)" in exI);
  apply (rule sym);
  apply (simp only: binomial_setprod_multiply_reduced);
  apply force;
  done;

lemma binomial_setprod_def: "k <= n ==> (n choose k) = setprod id {1..n} div ((setprod id {1..k})*(setprod id {1..(n-k)}))";
  apply (rule div_multiply);
  apply force;
  apply force;
  apply (rule sym);
  apply (subgoal_tac "(n choose k) * (setprod id {1::nat..k} * setprod id {1::nat..n - k}) = (setprod id {1..k})*(setprod id {1..(n-k)})*(n choose k)");
  apply (erule ssubst);
  apply (simp only: binomial_setprod_multiply div_multiply);
  apply force;
  done;

lemma binomial_eq: "a + b = n ==> (n choose a) = (n choose b)";
  apply (subgoal_tac "b = n - a");
  apply (erule ssubst);back;
  apply (rule binomial_sym);
  apply force+;
  done;

end;