proposition: Lemma lt_neq_creal (x y : creal) : (x < y)%CR -> x != y.
proof: Proof. move=> ltxy; pose_big_enough i. apply: (@neq_crealP (diff ltxy) i i) => //; first by rewrite diff_gt0. by rewrite distrC leNgt ltr_distl negb_and -!leNgt diffP ?orbT. 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)