proposition: Lemma lt_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 -> x i + e <= y j -> (x < y)%CR.
proof: Proof. move=> hi hj he; exists (e / 5%:R); rewrite pmulr_rgt0 ?gtr0E //=. rewrite ltW // (@gtr_creal (e / 5%:R) j) ?pmulr_rgt0 ?gtr0E //. rewrite (le_trans _ he) // -addrA (monoLR (addrNK _) (ler_add2r _)). rewrite ltW // (@ltr_creal (e / 5%:R) i) ?pmulr_rgt0 ?gtr0E //. rewrite -!addrA ler_addl !addrA -mulrA -{1}[e]mulr1 -!(mulrBr, mulrDr). rewrite pmulr_rge0 // {1}[1](splitf 5) /= !mul1r !mulrDr mulr1. by rewrite !opprD !addrA !addrK addrN. 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)