proposition: Lemma inject_Q_lt : forall q r : Q, Qlt q r -> inject_Q q < inject_Q r.
proof: Proof. intros q r Hlt. destruct (QarchimedeanExp2_Z (/(r-q))) as [n Hn]. rewrite Qinv_lt_contravar, Qinv_involutive, <- Qpower_opp in Hn. - exists (-n-1)%Z; cbn. rewrite Qpower_minus_pos; lra. - apply Qlt_shift_inv_l; lra. - apply Qpower_0_lt; lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra