proposition: Lemma scalerMnr a v n : a *: v *+ n = a *: (v *+ n).
proof: Proof. elim: n => [|n IHn]; first by rewrite !mulr0n scaler0. by rewrite !mulrSr IHn scalerDr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)