proposition: Lemma le_alg_def x y : le_alg x y = (x == y) || lt_alg x y.
proof: Proof. rewrite -[x]reprK -[y]reprK piE [lt_alg _ _]piE; apply/le_algcrealP/orP. move=> /le_creal_neqVlt [/eq_algcrealP/eqquotP/eqP-> //|lt_xy]; first by left. by right; apply/lt_algcrealP. by move=> [/eqP/eqquotP/eq_algcrealP-> //| /lt_algcrealP /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)