proposition: Lemma lboundP (x y : creal) (neq_xy : x != y) i : (cauchymod x (lbound neq_xy) <= i)%N -> (cauchymod y (lbound neq_xy) <= i)%N -> lbound neq_xy <= `|x i - y i|.
proof: Proof. rewrite /lbound; case: (sigW _)=> /= d /andP[d_gt0 hd] hi hj. apply: contraLR hd; rewrite -!ltNge=> hd. rewrite (@ltr_distl_creal d i) // distrC ltW // (@ltr_distl_creal d i) //. by rewrite distrC ltW // !mulrDr mulr1 !addrA !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)