proposition: Theorem inj_pow (n m : nat) : m <> 0 -> Pos.of_nat (n^m) = (Pos.of_nat n ^ Pos.of_nat m)%positive.
proof: Proof. intros Hm. apply Pos2Nat.inj. rewrite Pos2Nat.inj_pow. destruct n. - now rewrite Nat.pow_0_l, inj_0, Pos2Nat.inj_1, Nat.pow_1_l. - now rewrite !id; [..|apply Nat.pow_nonzero]. Qed.
imports: BinPos PeanoNat