proposition: Lemma pairMnE (M1 M2 : zmodType) (x : M1 * M2) n : x *+ n = (x.1 *+ n, x.2 *+ n).
proof: Proof. by case: x => x y; elim: n => //= n; rewrite !mulrS => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)