proposition: Lemma neq_creal_ltVgt (x y : creal) : x != y -> {(x < y)%CR} + {(y < x)%CR}.
proof: Proof. move=> neq_xy; pose_big_enough i. have := (@lboundP _ _ neq_xy i); big_enough => /(_ isT isT). have [le_xy|/ltW le_yx'] := lerP (x i) (y i). rewrite -(ler_add2r (x i)) ?addrNK addrC. move=> /lt_crealP; rewrite ?lbound_gt0; big_enough. by do 3!move/(_ isT); left. rewrite -(ler_add2r (y i)) ?addrNK addrC. move=> /lt_crealP; rewrite ?lbound_gt0; big_enough. by do 3!move/(_ isT); right. 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)