proposition: Lemma diff0P (x : creal) (x_gt0 : (0 < x)%CR) i : (cauchymod x (diff x_gt0) <= i)%N -> (cauchymod 0%CR (diff x_gt0) <= i)%N -> diff x_gt0 <= x i.
proof: Proof. by move=> cx c0; rewrite -[diff _]add0r -[0]/(0%CR i) diffP. 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)