proposition: Lemma ffunMzE (I : finType) (M : zmodType) (f : {ffun I -> M}) z x : (f *~ z) x = f x *~ z.
proof: Proof. by case: z => n; rewrite ?ffunE ffunMnE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)