proposition: Corollary creal_b_over_a_seq : creal_axiom b_over_a_seq.
proof: Proof. apply: (@asympt_eq_creal _ z3); exact: z3seq_b_over_a_asympt. 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