proposition: Lemma ltVge_algcreal_dec (x y : algcreal) : {(x < y)%CR} + {(y <= x)%CR}.
proof: Proof. have [eq_xy|/neq_creal_ltVgt [lt_xy|lt_yx]] := eq_algcreal_dec x y; by [right; rewrite eq_xy | left | right; apply: lt_crealW]. Qed.
imports: HB(structures) 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 generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)