proposition: Lemma DRealAbstr_aux : forall x H, isLowerCut (fun q : Q => if sig_forall_dec (fun n : nat => seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n)) (H q) then true else false).
proof: Proof. repeat split. - intros. destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= q + (2^-Z.of_nat n))%Q) (H q)). + reflexivity. + exfalso. destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= r + (2^-Z.of_nat n))%Q) (H r)). * destruct s. apply n. apply (Qle_trans _ _ _ (q0 x0)). apply Qplus_le_l. exact H0. * discriminate. - intro abs. destruct (Rfloor x) as [z [_ zmaj]]. specialize (abs (z+3 # 1)%Q). destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= (z+3 # 1) + (2^-Z.of_nat n))%Q) (H (z+3 # 1)%Q)). 2: exfalso; discriminate. clear abs. destruct s as [n nmaj]. apply nmaj. rewrite <- (inject_Q_plus (z#1) 2) in zmaj. apply CRealLt_asym in zmaj. rewrite <- CRealLe_not_lt in zmaj. specialize (zmaj (-Z.of_nat n)%Z). unfold inject_Q in zmaj; rewrite CReal_red_seq in zmaj. destruct x as [xn xcau]; rewrite CReal_red_seq in H, nmaj, zmaj |- *. rewrite Qinv_plus_distr in zmaj. apply (Qplus_le_l _ _ (-(z + 2 # 1))). apply (Qle_trans _ _ _ zmaj). apply (Qplus_le_l _ _ (-(2^-Z.of_nat n))). apply (Qle_trans _ 1). + ring_simplify. apply Qpower_2_neg_le_one. + ring_simplify. rewrite <- (Qinv_plus_distr z 3 1), <- (Qinv_plus_distr z 2 1). lra. - intro abs. destruct (Rfloor x) as [z [zmaj _]]. specialize (abs (z-4 # 1)%Q). destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= (z-4 # 1) + (2^-Z.of_nat n))%Q) (H (z-4 # 1)%Q)). + exfalso; discriminate. + clear abs. apply CRealLt_asym in zmaj. apply zmaj. clear zmaj. exists 0%Z. unfold inject_Q; rewrite CReal_red_seq. specialize (q O). destruct x as [xn xcau]. rewrite CReal_red_seq in H, q |- *. unfold Z.of_nat in q. change (2 ^ (- 0))%Q with 1%Q in q. change (-0)%Z with 0%Z in q. rewrite <- Qinv_minus_distr in q. change (2^0)%Q with 1%Q. lra. - intros q H0 abs. destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= q + (2^-Z.of_nat n))%Q) (H q)). 2: exfalso; discriminate. clear H0. destruct s as [n nmaj]. specialize (abs ((q + seq x (-Z.of_nat n) - (2^-Z.of_nat n)%Q)/2)%Q). destruct abs. + apply (Qmult_le_r _ _ 2) in H0. * field_simplify in H0. apply (Qplus_le_r _ _ ((2^-Z.of_nat n) - q)) in H0. ring_simplify in H0. apply nmaj. rewrite Qplus_comm. exact H0. * reflexivity. + destruct (sig_forall_dec (fun n0 : nat => (seq x (-Z.of_nat n0) <= (q + seq x (-Z.of_nat n) - (2^-Z.of_nat n)) / 2 + (2^-Z.of_nat n0))%Q) (H ((q + seq x (-Z.of_nat n) - (2^-Z.of_nat n)) / 2)%Q)). * discriminate. * clear H0. specialize (q0 n). apply (Qmult_le_l _ _ 2) in q0. -- field_simplify in q0. apply (Qplus_le_l _ _ (-seq x (-Z.of_nat n))) in q0. ring_simplify in q0. contradiction. -- reflexivity. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra