proposition: Lemma CRealLt_RQ_from_single_dist : forall (r : CReal) (q : Q) (n :Z), (2^n < q - seq r n)%Q -> r < inject_Q q.
proof: Proof. intros r q n Hapart. pose proof Qpower_0_lt 2 n ltac:(lra) as H2npos. destruct (QarchimedeanLowExp2_Z (q - seq r n - 2^n) ltac:(lra)) as [k Hk]. unfold CRealLt; exists (Z.min n (k-1))%Z. unfold inject_Q; rewrite CReal_red_seq. pose proof cauchy r n n (Z.min n (k-1))%Z ltac:(lia) ltac:(lia) as Hrbnd. pose proof Qpower_le_compat_l 2 (Z.min n (k - 1))%Z (k-1)%Z ltac:(lia) ltac:(lra). apply (Qmult_le_l _ _ 2 ltac:(lra)) in H. apply (Qle_lt_trans _ _ _ H); clear H. rewrite Qpower_minus_pos. simplify_Qlt. apply Qabs_Qlt_condition in Hrbnd. lra. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra