proposition: Lemma lt_creal_neq (x y : creal) : (x < y -> x != y)%CR.
proof: Proof. move=> lxy; pose_big_enough i. apply: (@neq_crealP (diff lxy) i i); rewrite ?diff_gt0 //. rewrite distrC ler_normr (monoRL (addrK _) (ler_add2r _)) addrC. by rewrite (diff_of lxy). by close. 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)