proposition: Lemma diffP (x y : creal) (lt_xy : (x < y)%CR) i : (cauchymod x (diff lt_xy) <= i)%N -> (cauchymod y (diff lt_xy) <= i)%N -> x i + diff lt_xy <= y i.
proof: Proof. rewrite /diff; case: (sigW _)=> /= e /andP[e_gt0 he] hi hj. rewrite ltW // (@gtr_creal e (cauchymod y e)) // (le_trans _ he) //. rewrite !mulrDr mulr1 !addrA !ler_add2r ltW //. by rewrite (@ltr_creal e (cauchymod x e)) // addrK. 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)