proposition: Lemma sub_alg_gt0 x y : lt_alg zero_alg (y - x) = lt_alg x y.
proof: Proof. rewrite -[x]reprK -[y]reprK !piE; apply/lt_algcrealP/lt_algcrealP=> /= hxy. pose_big_enough i. apply: (@lt_crealP _ (diff hxy) i i); rewrite ?diff_gt0 //. by rewrite (monoLR (addNKr _) (ler_add2l _)) addrC diff0P. by close. pose_big_enough i. apply: (@lt_crealP _ (diff hxy) i i); rewrite ?diff_gt0 //. by rewrite (monoRL (addrK _) (ler_add2r _)) add0r addrC diffP. by close. 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)