proposition: Lemma mul_na n b x: (cons zero n b) * x = (cons zero n zero) * x.
proof: Proof. by elim: x => // a' _ n' b' Hb /=; rewrite Hb //;case pa: (a'==zero). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)