proposition: Lemma CReal_from_cauchy_cm_mono : forall (n p : Z), (p <= n)%Z -> (CReal_from_cauchy_cm n <= CReal_from_cauchy_cm p)%positive.
proof: Proof. intros n p Hpn. unfold CReal_from_cauchy_cm; destruct n; destruct p; lia. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra