proposition: Lemma neq_crealP e i j (e_gt0 : 0 < e) (x y : creal) : (cauchymod x (e / 5%:R) <= i)%N -> (cauchymod y (e / 5%:R) <= j)%N -> e <= `|x i - y j| -> x != y.
proof: Proof. move=> hi hj he; exists (e / 5%:R); rewrite pmulr_rgt0 ?gtr0E //=. rewrite distrC ltW // (@ltr_distr_creal (e / 5%:R) j) ?pmulr_rgt0 ?gtr0E //. rewrite distrC ltW // (@ltr_distr_creal (e / 5%:R) i) ?pmulr_rgt0 ?gtr0E //. by rewrite mulr_natr -!mulrSr -mulrnAr -mulr_natr mulVf ?pnatr_eq0 ?mulr1. 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)