proposition: Lemma inj_pow x y : 0 < x -> 0 < y -> Z.to_pos (x^y) = (Z.to_pos x ^ Z.to_pos y)%positive.
proof: Proof. intros. apply Pos2Z.inj. rewrite Pos2Z.inj_pow, !id; trivial. apply Z.pow_pos_nonneg. - trivial. - now apply Z.lt_le_incl. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass