proposition: Lemma lt0_z3_minus_b_over_a (n : nat) : (2 <= n)%N -> (0%:CR < z3 - (b_over_a_seq n)%:CR)%CR.
proof: Proof. move=> le2n. pose_big_enough m. have diff_pos1 (k l : nat) : (k < l)%N -> (1 < k)%N -> 0 < b_over_a_seq l - b_over_a_seq k. move=> ltkn lt1k; rewrite Db_over_a_casoratian //. rewrite (big_cat_nat _ _ _ (leqnSn _) ltkn) big_nat1 /=. have aux (i : nat) : 0 < 6%:Q / (i%:Q + 1) ^ 3 / (a (int.shift 1 i) * a i). apply: divr_gt0; first by apply: lt_0_ba_casoratian. apply:mulr_gt0; exact: lt_0_a. apply/ltr_pwDl/sumr_ge0 => // i _; exact: ltW. have -> : (z3 - (b_over_a_seq n)%:CR == z3 - (b_over_a_seq m)%:CR + (b_over_a_seq m - b_over_a_seq n)%:CR)%CR. by apply: eq_creal_ext => i /=; ring. rewrite z3_eq_b_over_a; apply: ltcr_spaddr. apply/lt_creal_cst/diff_pos1; raise_big_enough. by apply: (@le_crealP _ m.+1) => *; apply/ltW/diff_pos1; raise_big_enough. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals) extra_mathcomp extra_cauchyreals tactics shift bigopz arithmetics seq_defs c_props s_props z3seq_props a_props b_props b_over_a_props