proposition: Lemma lreg_lead p : GRing.lreg (lead_coef p) -> GRing.lreg p.
proof: Proof. move/mulrI_eq0=> reg_p; apply: mulrI0_lreg => q /eqP; apply: contraTeq => nz_q. by rewrite -lead_coef_eq0 lead_coef_proper_mul reg_p lead_coef_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)