proposition: Lemma Qabs_Qgt_condition: forall x y : Q, (x < Qabs y)%Q <-> (x < y \/ x < -y)%Q.
proof: Proof. intros x y. apply Qabs_case; lra. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax