proposition: Lemma add_alg_gt0 x y : lt_alg zero_alg x -> lt_alg zero_alg y -> lt_alg zero_alg (x + y).
proof: Proof. rewrite -[x]reprK -[y]reprK !piE -!(rwP lt_algcrealP). move=> x_gt0 y_gt0; pose_big_enough i. apply: (@lt_crealP _ (diff x_gt0 + diff y_gt0) i i) => //. by rewrite addr_gt0 ?diff_gt0. by rewrite /= add0r ler_add // ?diff0P. 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)