Lemma Dcuts_plus_double : ∏ x : Dcuts, Dcuts_plus x x = Dcuts_mult Dcuts_two x. Proof. intros x. rewrite <- (Dcuts_NQmult_mult _ _ ispositive_twoNonnegativeRationals). apply Dcuts_eq_is_eq. intros r ; split. - apply hinhfun ; apply sumofmaps ; [ apply sumofmaps ; intros Xr | intros xy ; rewrite (pr1 (pr2 xy))]. + exists (r / 2)%NRat. simpl ; split. * apply pathsinv0, multdivNonnegativeRationals. exact ispositive_twoNonnegativeRationals. * apply is_Dcuts_bot with (1 := Xr). pattern r at 2 ; rewrite (NQhalf_double r). apply plusNonnegativeRationals_le_l. + exists (r / 2)%NRat. simpl ; split. * apply pathsinv0, multdivNonnegativeRationals. exact ispositive_twoNonnegativeRationals. * apply is_Dcuts_bot with (1 := Xr). pattern r at 2 ; rewrite (NQhalf_double r). apply plusNonnegativeRationals_le_l. + exists ((pr1 (pr1 xy) + pr2 (pr1 xy)) / 2)%NRat. split. * apply pathsinv0, multdivNonnegativeRationals. exact ispositive_twoNonnegativeRationals. * generalize (isdecrel_ltNonnegativeRationals (pr1 (pr1 xy)) (pr2 (pr1 xy))) ; apply sumofmaps ; intros H. { apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 xy))). pattern (pr2 (pr1 xy)) at 2 ; rewrite (NQhalf_double (pr2 (pr1 xy))). unfold divNonnegativeRationals. rewrite isrdistr_mult_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_r. apply multNonnegativeRationals_lecompat_r. now apply lt_leNonnegativeRationals. } apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 xy))). pattern (pr1 (pr1 xy)) at 2 ; rewrite (NQhalf_double (pr1 (pr1 xy))). unfold divNonnegativeRationals. rewrite isrdistr_mult_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. apply multNonnegativeRationals_lecompat_r. now apply notlt_geNonnegativeRationals. - apply hinhfun ; intros q ; rewrite (pr1 (pr2 q)). right. exists (pr1 q,,pr1 q). repeat split. + assert (X : (2 = 1+1)%NRat). { apply subtypePath_prop ; simpl. apply hq2eq1plus1. } pattern 2%NRat at 1 ; rewrite X ; clear X. rewrite isrdistr_mult_plusNonnegativeRationals, islunit_oneNonnegativeRationals. reflexivity. + exact (pr2 (pr2 q)). + 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.