proposition: Lemma inj_pow_pos x p : 0 < x -> Z.to_pos (Z.pow_pos x p) = ((Z.to_pos x)^p)%positive.
proof: Proof. intros. now apply (inj_pow x (Z.pos p)). Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass