proposition: Lemma mleadc_eq0 p : (p@_(mlead p) == 0) = (p == 0).
proof: Proof. apply/idP/idP => [|/eqP->]; last by rewrite mcoeff0. by case: (p =P 0) => // /eqP /mlead_supp; rewrite mcoeff_eq0 => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg