proposition: Lemma DRealQuot2 : forall x:CReal, CRealEq (DRealRepr (DRealAbstr x)) x.
proof: Proof. split. - intros [p pmaj]. unfold DRealRepr in pmaj. rewrite CReal_red_seq in pmaj. destruct (Z_ge_lt_dec 0 p) as [Hdec|Hdec]. + unfold CReal_of_DReal_seq in pmaj. destruct (DRealQlimExp2 (DRealAbstr x) (Z.to_nat (- p))) as [q [Hql Hqr]]. unfold proj1_sig in pmaj. pose proof (DRealAbstrFalse x _ (Z.to_nat (- p)) Hqr) as Hq; clear Hql Hqr. rewrite <- Qpower_2_neg_eq_natpow_inv in Hq. rewrite Z2Nat.id, Z.opp_involutive in Hq by lia; clear Hdec. lra. + rewrite CReal_of_DReal_seq_max_prec_1 in pmaj by lia. unfold CReal_of_DReal_seq in pmaj. change (Z.to_nat (-0))%Z with 0%nat in pmaj. destruct (DRealQlimExp2 (DRealAbstr x) 0) as [q [Hql Hqr]]. unfold proj1_sig in pmaj. pose proof (DRealAbstrFalse'' x _ p%nat Hqr) as Hq; clear Hql Hqr. rewrite <- Qpower_2_neg_eq_natpow_inv in Hq. change (- Z.of_nat 0)%Z with 0%Z in Hq. pose proof (Qpower_le_compat_l 2 1 p ltac:(lia) ltac:(lra)) as Hpowle. change (2^1)%Q with 2%Q in Hpowle. lra. - intros [p pmaj]. unfold DRealRepr in pmaj. rewrite CReal_red_seq in pmaj. unfold CReal_of_DReal_seq in pmaj. destruct (DRealQlimExp2 (DRealAbstr x) (Z.to_nat (- p))) as [q [Hql Hqr]]. unfold proj1_sig in pmaj. unfold DRealAbstr, proj1_sig in Hql. match type of Hql with context [ if ?a then _ else _ ] => destruct a as [H'|H']end. 2: discriminate. clear Hql Hqr. destruct H' as [n nmaj]. apply nmaj; clear nmaj. apply (Qplus_lt_l _ _ (seq x p + 2 ^ (- Z.of_nat n))) in pmaj. ring_simplify in pmaj. apply Qlt_le_weak. rewrite Qplus_comm. apply (Qlt_trans _ ((2 * 2^p) + seq x p + (2 ^ (- Z.of_nat n)))). 2: exact pmaj. clear pmaj. apply (Qplus_lt_l _ _ (-seq x p)). apply (Qle_lt_trans _ _ _ (Qle_Qabs _)). destruct (Z_le_gt_dec p (- Z.of_nat n)). + apply (Qlt_trans _ (2 ^ (- Z.of_nat n))). 1: apply (cauchy x). 1, 2: lia. pose proof Qpower_0_lt 2 p; lra. + apply (Qlt_trans _ (2^p)). 1: apply (cauchy x). 1, 2: lia. pose proof Qpower_0_lt 2 (- Z.of_nat n). pose proof Qpower_0_lt 2 p. lra. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra