proposition: Lemma CReal_of_DReal_cauchy (x : DReal) : QCauchySeq (CReal_of_DReal_seq x).
proof: Proof. unfold QCauchySeq, CReal_of_DReal_seq. intros n k l Hk Hl. destruct (DRealQlimExp2 x (Z.to_nat (-k))) as [q Hq]. destruct (DRealQlimExp2 x (Z.to_nat (-l))) as [r Hr]. destruct x as [f Hflc]. unfold proj1_sig in *. apply Qabs_case. - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (2 ^ Z.to_nat (-l)))). + apply (Qplus_lt_l _ _ r); ring_simplify. apply (UpperAboveLower f). * exact Hflc. * apply Hq. * apply Hr. + apply (Qle_trans _ _ _ (Qpower_2_invneg_le_pow _)). apply Qpower_le_compat_l; [lia|lra]. - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (2 ^ Z.to_nat (-k)))). + apply (Qplus_lt_l _ _ q); ring_simplify. apply (UpperAboveLower f). * exact Hflc. * apply Hr. * apply Hq. + apply (Qle_trans _ _ _ (Qpower_2_invneg_le_pow _)). apply Qpower_le_compat_l; [lia|lra]. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra