proposition: Lemma CRealArchimedean : forall x:CReal, { n:Z & x < inject_Z n < x+2 }.
proof: Proof. intros x. remember (seq x (-3)%Z + (3#2))%Q as q eqn: Heqq. pose proof (Qlt_floor q) as Hltfloor; unfold QArith_base.inject_Z in Hltfloor. pose proof (Qfloor_le q) as Hfloorle; unfold QArith_base.inject_Z in Hfloorle. exists (Qfloor q); split. - unfold inject_Z, inject_Q, CRealLt. rewrite CReal_red_seq. exists (-3)%Z. setoid_replace (2 * 2 ^ (-3))%Q with (1#4)%Q by reflexivity. subst q; rewrite <- Qinv_plus_distr in Hltfloor. lra. - unfold inject_Z, inject_Q, CReal_plus, CReal_plus_seq, CRealLt. do 3 rewrite CReal_red_seq. exists (-3)%Z. setoid_replace (2 * 2 ^ (-3))%Q with (1#4)%Q by reflexivity. simplify_seq_idx; rewrite Qred_correct. pose proof cauchy x (-3)%Z (-3)%Z (-4)%Z ltac:(lia) ltac:(lia) as Hbnddx. rewrite Qabs_Qlt_condition in Hbnddx. setoid_replace (2 ^ (-3))%Q with (1#8)%Q in Hbnddx by reflexivity. subst q; rewrite <- Qinv_plus_distr in Hltfloor. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra