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