proposition: Lemma asympt_eq_creal (x : creal F) (y : nat -> F) : {asympt e : i / `|x i - y i| < e} -> creal_axiom y.
proof: Proof. case: x => x [mx mxP]; case=> M MP; exists_big_modulus m F. move=> eps i j lt_eps_0 hmi hmj; pose d (k : nat) := x k - y k. have -> : y i - y j = d j + (x i - x j) - d i. rewrite /d [(_ - _) + _]addrC addrA addrNK opprB addrA [_ - x i]addrC. by rewrite addrA addKr addrC. suff step1 : `|d j + (x i - x j)| + `|d i| < eps. by apply: le_lt_trans step1; rewrite -[`|d i|]normrN; apply: ler_normD. suff step2 : `|d j| + `|x i - x j| + `|d i| < eps. by apply: le_lt_trans step2; rewrite lerD2r; apply: ler_normD. have -> : eps = eps / 3%:~R + eps / 3%:~R + eps / 3%:~R. rewrite /= in eps lt_eps_0 hmi hmj *. rewrite -!mulrDl -[in X in _ = X](mulr1 eps) -!mulrDr -mulrA. suff -> : (1 + 1 + 1) / 3%:~R = 1 :> F by rewrite mulr1. rewrite -[X in (X + X + X) / _ = _]/(1%:~R) -!rmorphD /= mulfV //. by rewrite intr_eq0. have heps : 0 < eps / 3%:~R by apply: divr_gt0 => //; rewrite ltr0z. apply: ltrD => //; last exact: MP. apply: ltrD=> //; first by exact: MP. by move=> {MP}; apply: mxP. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)