proposition: Lemma mul_creal_neq0 x y : x != 0 -> y != 0 -> x * y != 0.
proof: Proof. move=> x_neq0 y_neq0. pose d := lbound x_neq0 * lbound y_neq0. have d_gt0 : 0 < d by rewrite pmulr_rgt0 lbound_gt0. pose_big_enough i. apply: (@neq_crealP d i i)=> //; rewrite subr0 normrM. apply: le_trans (_ : `|x i| * lbound y_neq0 <= _). by rewrite ler_wpmul2r ?lbound_ge0 // lbound0P. by rewrite ler_wpmul2l ?normr_ge0 // lbound0P. by close. Qed.
imports: 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 bigenough)