Lemma Dcuts_inv_open : Dcuts_def_open Dcuts_inv_val. Proof. intros r. apply hinhuniv. intros l. generalize (eq0orgt0NonnegativeRationals r) ; apply sumofmaps ; intros Hr0. - rewrite Hr0 in l |- * ; clear r Hr0. revert X_finite. apply hinhfun. intros r'. set (r := NQmax 2%NRat (pr1 r')). assert (Hr1 : (1 < r)%NRat). { apply istrans_lt_le_ltNonnegativeRationals with (2 := NQmax_le_l _ _). exact one_lt_twoNonnegativeRationals. } assert (Hr0 : (0 < r)%NRat). { simple refine (istrans_le_lt_ltNonnegativeRationals _ _ _ _ Hr1). now apply isnonnegative_NonnegativeRationals. } exists (/ (r * r))%NRat ; split. + apply hinhpr. exists (/ r)%NRat ; repeat split. * intros rx Xrx. apply (multNonnegativeRationals_lecompat_l' (r * r)). ** now apply ispositive_multNonnegativeRationals. ** rewrite <- isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, islunit_oneNonnegativeRationals. *** rewrite isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals. **** apply istrans_leNonnegativeRationals with (2 := NQmax_le_r _ _). apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals ; intro H ; apply (pr2 r'). now apply X_bot with (1 := Xrx). **** exact Hr0. *** now apply ispositive_multNonnegativeRationals. * now apply ispositive_invNonnegativeRationals. * apply_pr2 (multNonnegativeRationals_ltcompat_l r). ** assumption. ** now rewrite isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals. + apply ispositive_invNonnegativeRationals. now apply ispositive_multNonnegativeRationals. - set (l' := between_ltNonnegativeRationals _ _ (pr2 (pr2 (pr2 l)))). apply hinhpr. exists ((pr1 l'/pr1 l) * r)%NRat ; split. + apply hinhpr. exists (pr1 l') ; repeat split. * intros rx Xrx. rewrite isassoc_multNonnegativeRationals. pattern l' at 1 ; rewrite <- (multdivNonnegativeRationals (pr1 l') (pr1 l)), iscomm_multNonnegativeRationals. ** apply multNonnegativeRationals_lecompat_r. now apply (pr1 (pr2 l)). ** exact (pr1 (pr2 (pr2 l))). * apply istrans_le_lt_ltNonnegativeRationals with (2 := pr1 (pr2 l')). now apply isnonnegative_NonnegativeRationals. * exact (pr2 (pr2 l')). + pattern r at 1 ; rewrite <- (islunit_oneNonnegativeRationals r). apply multNonnegativeRationals_ltcompat_r. * exact Hr0. * apply_pr2 (multNonnegativeRationals_ltcompat_r (pr1 l)). ** exact (pr1 (pr2 (pr2 l))). ** rewrite islunit_oneNonnegativeRationals. rewrite iscomm_multNonnegativeRationals, multdivNonnegativeRationals. *** exact (pr1 (pr2 l')). *** exact (pr1 (pr2 (pr2 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.