proposition: Lemma Pos2Z_pos_is_pos : forall (p : positive), (1 <= Z.pos p)%Z.
proof: Proof. intros p. lia. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax