Library Coq.Reals.Cauchy.PosExtra

Require Import PArith.
Require Import ZArith.
Require Import Lia.

Lemma Pos_pow_1_r: forall p : positive,
  (1^p = 1)%positive.

Lemma Pos_le_multiple : forall n p : positive, (n <= p * n)%positive.

Lemma Pos_pow_le_mono_r : forall a b c : positive,
    (b <= c)%positive
 -> (a ^ b <= a ^ c)%positive.