proposition: Lemma CReal_injectQPos : forall q : Q, (0 < q)%Q -> CRealLt (inject_Q 0) (inject_Q q).
proof: Proof. intros q Hq. destruct (QarchimedeanExp2_Z ((2#1) / q)) as [k Hk]. exists (-k)%Z; cbn. apply (Qmult_lt_compat_r _ _ q) in Hk. 2: assumption. apply (Qmult_lt_compat_r _ _ (2^(-k))) in Hk. 2: apply Qpower_0_lt; lra. field_simplify in Hk. 2: lra. rewrite <- Qmult_assoc, <- Qpower_plus in Hk by lra. ring_simplify (-k +k)%Z in Hk. rewrite Qpower_0_r in Hk. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra