proposition: Lemma eq_crealP (x y : creal) : {asympt e : i / `|x i - y i| < e} -> (x == y)%CR.
proof: Proof. case=> m hm neq_xy; pose d := lbound neq_xy. pose_big_enough i. have := (hm d i); rewrite lbound_gt0; big_enough => /(_ isT isT). by apply/negP; rewrite -leNgt lboundP. by close. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)