proposition: Lemma Qnot_lt_iff_le: forall x y : Q, ~ (x < y)%Q <-> (y <= x)%Q.
proof: Proof. intros x y; split. - apply Qnot_lt_le. - apply Qle_not_lt. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax