Lemma Dcuts_inv_corr_aux : Dcuts_def_corr Dcuts_inv_val. Proof. assert (∏ c, (0 < c)%NRat -> hexists (λ q : NonnegativeRationals, X q × ¬ X (q + c))). { intros c Hc0. generalize (X_corr c Hc0) ; apply hinhuniv ; apply sumofmaps ; [ intros nXc | intros H]. - apply hinhpr. exists 0%NRat ; split. + exact X_0. + now rewrite islunit_zeroNonnegativeRationals. - apply hinhpr ; exact H. } clear X_corr ; rename X0 into X_corr. intros c Hc0. apply ispositive_NQhalf in Hc0. specialize (X_corr _ Hc0) ; revert X_corr. apply hinhfun ; intros r. right. exists (/ (NQmax 1%NRat (pr1 r) + c))%NRat ; split. - apply Dcuts_inv_out with (1 := pr2 (pr2 r)). pattern c at 2; rewrite (NQhalf_double c), <- isassoc_plusNonnegativeRationals. eapply istrans_le_lt_ltNonnegativeRationals, plusNonnegativeRationals_lt_r. + apply plusNonnegativeRationals_lecompat_r ; apply NQmax_le_r. + exact Hc0. - assert (Xmax : X (NQmax 1%NRat (pr1 r))). { apply NQmax_case. { exact X_1. } exact (pr1 (pr2 r)). } assert (Hmax : (0 < NQmax 1 (pr1 r))%NRat). { eapply istrans_lt_le_ltNonnegativeRationals, NQmax_le_l. now eapply ispositive_oneNonnegativeRationals. } intro Hinv ; apply (Dcuts_inv_in _ Hmax Xmax), Dcuts_inv_bot with (1 := Hinv). apply lt_leNonnegativeRationals, minusNonnegativeRationals_ltcompat_l' with (/ (NQmax 1 (pr1 r) + c))%NRat. rewrite plusNonnegativeRationals_minus_l. rewrite minus_divNonnegativeRationals, plusNonnegativeRationals_minus_l. * unfold divNonnegativeRationals ; apply_pr2 (multNonnegativeRationals_ltcompat_r (NQmax 1 (pr1 r) * (NQmax 1 (pr1 r) + c))%NRat). ** apply ispositive_multNonnegativeRationals. *** exact Hmax. *** now apply ispositive_plusNonnegativeRationals_l. ** rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals. *** apply multNonnegativeRationals_ltcompat_l. { now apply_pr2 ispositive_NQhalf. } pattern 1%NRat at 1 ; rewrite <- (islunit_oneNonnegativeRationals 1%NRat). apply istrans_le_lt_ltNonnegativeRationals with (NQmax 1 (pr1 r) * 1)%NRat. { now apply multNonnegativeRationals_lecompat_r, NQmax_le_l. } apply multNonnegativeRationals_ltcompat_l. { exact Hmax. } apply istrans_le_lt_ltNonnegativeRationals with (1 := NQmax_le_l _ (pr1 r)). apply plusNonnegativeRationals_lt_r. now apply_pr2 ispositive_NQhalf. *** apply ispositive_multNonnegativeRationals. { exact Hmax. } now apply ispositive_plusNonnegativeRationals_l. * now apply ispositive_plusNonnegativeRationals_l. Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.