proposition: Lemma lt_0_sigma (n : nat) : (2 <= n)%N -> (0%CR < sigma n)%CR.
proof: Proof. move=> le2n; rewrite /sigma -!cst_crealM; apply: mulr_gtcr0. by apply/lt_creal_cst; rewrite mulr_gt0 // exprz_gt0 ?ltr0n. suff : (0 < (a n)%:CR * (z3 - (b_over_a_seq n)%:CR))%CR. by rewrite mulcrDr mulcrN -cst_crealM mulrC mulfVK // a_neq0. exact/mulr_gtcr0/lt0_z3_minus_b_over_a/le2n/lt_creal_cst/lt_0_a. 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