proposition: Lemma mleadZ c p : c != 0 -> mlead (c *: p) = mlead p.
proof: Proof. move=> nz_c; have [->|nz_p] := eqVneq p 0; first by rewrite scaler0. by rewrite mleadZ_proper // mulf_neq0 // mleadc_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