proposition: Lemma CRlt_lpo_dec : forall {R : ConstructiveReals} (x y : CRcarrier R), (forall (P : nat -> Prop), (forall n, {P n} + {~P n}) -> {n | ~P n} + {forall n, P n}) -> sum (x < y) (y <= x).
proof: Proof. intros R x y lpo. assert (forall (z:CRcarrier R) (n : nat), z < z + CR_of_Q R (1 # Pos.of_nat (S n))). { intros. apply (CRle_lt_trans _ (z+0)). - rewrite CRplus_0_r. apply CRle_refl. - apply CRplus_lt_compat_l. apply CR_of_Q_pos. reflexivity. } pose (fun n:nat => let (q,_) := CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat (S n))) (H x n) in q) as xn. pose (fun n:nat => let (q,_) := CR_Q_dense R y (y + CR_of_Q R (1 # Pos.of_nat (S n))) (H y n) in q) as yn. destruct (lpo (fun n => Qle (yn n) (xn n + (1 # Pos.of_nat (S n))))). - intro n. destruct (Q_dec (yn n) (xn n + (1 # Pos.of_nat (S n)))). + destruct s. * left. apply Qlt_le_weak, q. * right. apply (Qlt_not_le _ _ q). + left. rewrite q. apply Qle_refl. - left. destruct s as [n nmaj]. apply Qnot_le_lt in nmaj. apply (CRlt_le_trans _ (CR_of_Q R (xn n))). + unfold xn. destruct (CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat (S n))) (H x n)). exact (fst p). + apply (CRle_trans _ (CR_of_Q R (yn n - (1 # Pos.of_nat (S n))))). * apply CR_of_Q_le. rewrite <- (Qplus_le_l _ _ (1# Pos.of_nat (S n))). ring_simplify. apply Qlt_le_weak, nmaj. * unfold yn. destruct (CR_Q_dense R y (y + CR_of_Q R (1 # Pos.of_nat (S n))) (H y n)). unfold Qminus. rewrite CR_of_Q_plus, CR_of_Q_opp. apply (CRplus_le_reg_r (CR_of_Q R (1 # Pos.of_nat (S n)))). rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRlt_asym, (snd p). - right. apply (CR_cv_le (fun n => CR_of_Q R (yn n)) (fun n => CR_of_Q R (xn n) + CR_of_Q R (1 # Pos.of_nat (S n)))). + intro n. rewrite <- CR_of_Q_plus. apply CR_of_Q_le. exact (q n). + intro p. exists (Pos.to_nat p). intros. unfold yn. destruct (CR_Q_dense R y (y + CR_of_Q R (1 # Pos.of_nat (S i))) (H y i)). rewrite CRabs_right. * apply (CRplus_le_reg_r y). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm. apply (CRle_trans _ (y + CR_of_Q R (1 # Pos.of_nat (S i)))). -- apply CRlt_asym, (snd p0). -- apply CRplus_le_compat_l. apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. ++ apply le_S, H0. ++ discriminate. * rewrite <- (CRplus_opp_r y). apply CRplus_le_compat_r, CRlt_asym, p0. + apply (CR_cv_proper _ (x+0)). 2: rewrite CRplus_0_r; reflexivity. apply CR_cv_plus. * intro p. exists (Pos.to_nat p). intros. unfold xn. destruct (CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat (S i))) (H x i)). rewrite CRabs_right. -- apply (CRplus_le_reg_r x). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm. apply (CRle_trans _ (x + CR_of_Q R (1 # Pos.of_nat (S i)))). ++ apply CRlt_asym, (snd p0). ++ apply CRplus_le_compat_l. apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. ** apply le_S, H0. ** discriminate. -- rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r, CRlt_asym, p0. * intro p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right. -- apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. ++ apply le_S, H0. ++ discriminate. -- apply CR_of_Q_le. discriminate. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon