proposition: Lemma inj_pow n m : 0<=m -> Z.abs_N (n^m) = ((Z.abs_N n)^(Z.abs_N m))%N.
proof: Proof. intros Hm. rewrite abs_N_spec, Z.abs_pow, Z2N.inj_pow, <- abs_N_spec; trivial. - f_equal. symmetry; now apply abs_N_nonneg. - apply Z.abs_nonneg. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat