proposition: Lemma inj_pow a a' : N.to_nat (a ^ a') = N.to_nat a ^ N.to_nat a'.
proof: Proof. destruct a, a'; [easy| |easy|apply Pos2Nat.inj_pow]. now rewrite N.pow_0_l, Nat.pow_0_l; [|rewrite <- inj_0; intros ? %inj|]. Qed.
imports: BinPos BinNat PeanoNat Pnat