proposition: Lemma my_pow_m3lmul m p : m3lmx (my_pow m3lmul m p) = my_pow *%R (m3lmx m) p.
proof: Proof. rewrite /my_pow. have : GRing.comm (m3lmx m) (m3lmx m) by []. elim: (behead (bits p [::])) {1 4 6}m => [ | b bits Ih] acc comh //. rewrite /=. have comma2m : GRing.comm (m3lmx acc * m3lmx acc) (m3lmx m). by rewrite /GRing.comm -mulrA comh !mulrA comh. case: b; rewrite Ih !m3lmulP //. by rewrite /GRing.comm comma2m -(mulrA (m3lmx m)) comma2m. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)