proposition: Lemma Dcuts_half_double : ∏ x : Dcuts, x = Dcuts_plus (Dcuts_half x) (Dcuts_half x).
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals