Lemma Dcuts_of_Dcuts_bij : ∏ x : Dcuts, Dcuts_of_Dcuts (Dcuts_of_Dcuts'_val (pr1 x)) (Dcuts_of_Dcuts'_bot (pr1 x)) (Dcuts_of_Dcuts'_corr (pr1 x) (is_Dcuts_bot x) (is_Dcuts_corr x)) = x. Proof. intros x. apply Dcuts_eq_is_eq. intros r. split. - apply hinhuniv. intros y. generalize (pr1 (pr2 y)). apply hinhuniv. intros q. apply is_Dcuts_bot with (1 := pr2 (pr2 q)). apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals. intro H. apply (pr1 (pr2 q)). now apply is_Dcuts_bot with (1 := pr2 (pr2 y)). - intros Xr. generalize (is_Dcuts_open _ _ Xr). apply hinhfun. intros q. exists (NonnegativeRationals_to_Dcuts (pr1 q)). split. + apply hinhpr. exists (pr1 q). split. * simpl. now apply isirrefl_ltNonnegativeRationals. * exact (pr1 (pr2 q)). + simpl. exact (pr2 (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.