Lemma islunit_Dcuts_mult_one : islunit Dcuts_mult Dcuts_one. Proof. intros x. apply Dcuts_eq_is_eq ; intro r ; split. - apply hinhuniv ; intros ix. apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 ix))). pattern r at 1 ; rewrite (pr1 (pr2 ix)), iscomm_multNonnegativeRationals. apply multNonnegativeRationals_le1_r, lt_leNonnegativeRationals. exact (pr1 (pr2 (pr2 ix))). - intros Xr. generalize (is_Dcuts_open x r Xr). apply hinhfun ; intros q. exists ((r/pr1 q)%NRat,,pr1 q) ; repeat split. + simpl. rewrite iscomm_multNonnegativeRationals, multdivNonnegativeRationals. * reflexivity. * apply istrans_le_lt_ltNonnegativeRationals with (2 := pr2 (pr2 q)). apply isnonnegative_NonnegativeRationals. + change (r / pr1 q < 1)%NRat. apply_pr2 (multNonnegativeRationals_ltcompat_l (pr1 q)). * apply istrans_le_lt_ltNonnegativeRationals with (2 := pr2 (pr2 q)). apply isnonnegative_NonnegativeRationals. * rewrite multdivNonnegativeRationals, isrunit_oneNonnegativeRationals. ** exact (pr2 (pr2 q)). ** apply istrans_le_lt_ltNonnegativeRationals with (2 := pr2 (pr2 q)). apply isnonnegative_NonnegativeRationals. + exact (pr1 (pr2 q)). 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.