proposition: Lemma exprZn k x n : (k *: x) ^+ n = k ^+ n *: x ^+ n.
proof: Proof. elim: n => [|n IHn]; first by rewrite !expr0 scale1r. by rewrite !exprS IHn -scalerA scalerAr scalerAl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)