proposition: Lemma Pos_pow_le_mono_r : forall a b c : positive, (b <= c)%positive -> (a ^ b <= a ^ c)%positive.
proof: Proof. intros a b c. pose proof Z.pow_le_mono_r (Z.pos a) (Z.pos b) (Z.pos c). lia. Qed.
imports: PArith ZArith Lia