fact: Definition sigma (n : nat) := (2%:Q%:CR * ((l n)%:Q ^ 3)%:CR * ((a n)%:CR * z3 - (b n)%:CR))%CR.
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