proposition: Lemma creal_neq_always (x y : creal) i (neq_xy : x != y) : (cauchymod x (lbound neq_xy) <= i)%N -> (cauchymod y (lbound neq_xy) <= i)%N -> (x i != y i)%B.
proof: Proof. move=> hx hy; rewrite -subr_eq0 -normr_gt0. by rewrite (lt_le_trans _ (lbound_of neq_xy)) ?lbound_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)