Lemma Dcuts_half_double : ∏ x : Dcuts, x = Dcuts_plus (Dcuts_half x) (Dcuts_half x). Proof. intros x. rewrite <- isdistr_Dcuts_half_plus. apply Dcuts_eq_is_eq ; split. - intros Hr. apply hinhpr ; right ; exists (r,,r). now repeat split. - apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps | intros xy ]. + now simple refine (Dcuts_half_le _ _). + now simple refine (Dcuts_half_le _ _). + generalize (isdecrel_ltNonnegativeRationals r (pr1 (pr1 xy))) ; apply sumofmaps ; intro Hrx. * apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 xy))). now apply lt_leNonnegativeRationals. * apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_l r). pattern (r+r) at 1 ; rewrite (pr1 (pr2 xy)). apply plusNonnegativeRationals_lecompat_r. now apply notlt_geNonnegativeRationals. 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.