proposition: Lemma le_inject_Q : forall q r : Q, inject_Q q <= inject_Q r -> (q <= r)%Q.
proof: Proof. intros q r Hle. destruct (Qlt_le_dec r q) as [Hdec|Hdec]. - exfalso. apply Hle; apply inject_Q_lt; exact Hdec. - exact Hdec. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra