proposition: Fact z3_eq_b_over_a : (z3 == b_over_a)%CR.
proof: Proof. exact/eq_crealP/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