proposition: Lemma my_pow_m2lmul m p : m2lmx (my_pow m2lmul m p) = my_pow *%R (m2lmx m) p.
proof: Proof. rewrite /my_pow. elim: (behead (bits p [::])) {2 4}m => [ | b bits Ih] acc //=. by case: b; rewrite Ih !m2lmulP. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)