proposition: Lemma mul_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 pmulr_rgt0 ?diff_gt0. rewrite /= add0r (le_trans (_ : _ <= diff x_gt0 * (repr y) i)) //. by rewrite ler_wpmul2l ?(ltW (diff_gt0 _)) // diff0P. by rewrite ler_wpmul2r ?diff0P ?ltW ?creal_gt0_always. 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)