proposition: Lemma w_upper_bounded k : w_seq k <= w%:C.
proof: Proof. wlog le4k : k / (4 <= k)%N. move=> hwlog; case: (leqP 4 k) => [|ltk4]; first exact: hwlog. apply: le_trans (hwlog 4%N _) => //; apply: w_seq_incr; exact: ltnW. rewrite -(subnK le4k) addnC; apply: le_trans (w_seq_bound_tail _ _) _ => //. have -> : w_seq 4 = a' 0 * a' 1 * a' 2 * a' 3. by rewrite /w_seq !big_ord_recr /= big_ord0 mul1r. have a'0_ubP : a' 0 <= a'0_ub%:C. have ge0a'0 : 0 <= a'0_ub%:C by rewrite ler0q divr_ge0. by rewrite root_le_x // a0 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia. have a'1_ubP : a' 1 <= a'1_ub%:C. have ge0a'1 : 0 <= a'1_ub%:C by rewrite ler0q divr_ge0. by rewrite root_le_x // a1 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia. have a'2_ubP : a' 2 <= a'2_ub%:C. have ge0a'2 : 0 <= a'2_ub%:C by rewrite ler0q divr_ge0. have ge0a2 : 0 <= (a 2)%:Q%:C by rewrite ler0q. by rewrite root_le_x // a2 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia. have a'3_ubP : a' 3 <= a'3_ub%:C. have ge0a'3 : 0 <= a'3_ub%:C by rewrite ler0q divr_ge0. have ge0a3 : 0 <= (a 3)%:Q%:C by rewrite ler0q. by rewrite root_le_x // a3 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia. have a'4_ubP : a' 4 <= a'4_ub%:C. have ge0a'1 : 0 <= a'4_ub%:C by rewrite ler0q divr_ge0. have ge0a4 : 0 <= (a 4)%:Q%:C by rewrite ler0q ler0z. rewrite root_le_x //. pose t : rat := (rat_of_Z 200)^-1. have -> : a'4_ub = 1 + t by rewrite /a'4_ub /t; field. rewrite -rmorphXn ler_rat a4 exprDn. change 1808%N with (8 + 1800)%N. rewrite big_split_ord /=; apply: ler_wpDr. apply: sumr_ge0 => i. by rewrite expr1n mul1r mulrn_wge0 ?exprn_ge0 ?invr_ge0. rewrite 8!big_ord_recl big_ord0 !expr1n !mul1r /= /bump !add1n. set lhs := (X in _ <= X). suff -> : lhs = rat_of_Z 34077892883014859211 / rat_of_Z 12800000000000000. by rewrite lter_pdivlMr; ring_lia. rewrite {}/lhs bin0 mulr1n bin1 expr0 expr1. have -> : t ^+ 7 *+ 'C(1807, 7) = t ^+ 7 * rat_of_Z 12337390971384003811. rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=. by field. have -> : t ^+ 6 *+ 'C(1807, 6) = t ^+ 6 * rat_of_Z 47952102609488077. rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=. by field. have -> : t ^+ 5 *+ 'C(1807, 5) = t ^+ 5 * rat_of_Z 159662938766331. rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=. by field. have -> : t ^+ 4 *+ 'C(1807, 4) = t ^+ 4 * rat_of_Z 442770212885. rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=. by field. have -> : t ^+ 3 *+ 'C(1807, 3) = t ^+ 3 * rat_of_Z 981752135. rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=. by field. have -> : t ^+ 2 *+ 'C(1807, 2) = t ^+ 2 * rat_of_Z 1631721. rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=. by field. by rewrite /t; field. by rewrite 4!rmorphM rmorphXn /=; do 4!rewrite ler_pM ?mulr_ge0 //. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis