proposition: Lemma lt_inject_Q : forall q r : Q, inject_Q q < inject_Q r -> (q < r)%Q.
proof: Proof. intros q r [n Hn]; cbn in Hn. apply Qlt_minus_iff. assert(2^n>0)%Q by (apply Qpower_0_lt; lra); lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra