proposition: Lemma mul_neq0_creal x y : x * y != 0 -> y != 0.
proof: Proof. move=> xy_neq0; pose_big_enough i. apply: (@neq_crealP ((ubound x)^-1 * lbound xy_neq0) i i) => //. by rewrite pmulr_rgt0 ?invr_gt0 ?lbound_gt0 ?ubound_gt0. rewrite subr0 ler_pdivr_mull ?ubound_gt0 //. have /(_ i)-> // := (le_trans (lbound0_of xy_neq0)). by rewrite normrM ler_wpmul2r ?normr_ge0 ?uboundP. 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)