proposition: Lemma creal_lt_always (x y : creal) i (lt_xy : (x < y)%CR) : (cauchymod x (diff lt_xy) <= i)%N -> (cauchymod y (diff lt_xy) <= i)%N -> x i < y i.
proof: Proof. by move=> hx hy; rewrite (lt_le_trans _ (diff_of lt_xy)) ?ltr_addl ?diff_gt0. 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)