proposition: Lemma expnM m n1 n2 : m ^ (n1 * n2) = (m ^ n1) ^ n2.
proof: Proof. elim: n1 => [|n1 IHn]; first by rewrite exp1n. by rewrite expnD expnS expnMn IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring