proposition: Lemma pos2nat_inj_exp x y : Pos.to_nat (x ^ y) = Pos.to_nat x ^ Pos.to_nat y.
proof: Proof. have pos2nat_pow_xO a b (hab : Pos.to_nat (a ^ b) = Pos.to_nat a ^ Pos.to_nat b) : Pos.to_nat (a ^ b~0) = (Pos.to_nat a ^ Pos.to_nat b) ^ 2. by rewrite -Z2Nat.inj_pos Pos2Z.inj_pow Pos2Z.inj_xO Z.mul_comm Z.pow_mul_r // Z.pow_2_r -Pos2Z.inj_pow Z2Nat.inj_mul // Z2Nat.inj_pos multE hab mulnn. elim: y=> [y ihy|y ihy|]. by rewrite Pos2Nat.inj_xI multE expnS [in _ ^ _]mulnC expnM Pos.xI_succ_xO Pos.pow_succ_r Pos2Nat.inj_mul multE pos2nat_pow_xO. by rewrite Pos2Nat.inj_xO multE mulnC expnM pos2nat_pow_xO. by rewrite Pos2Nat.inj_1 expn1 Pos.pow_1_r. Qed.
imports: ZArith Lia mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements pos)