proposition: Lemma isdistr_Dcuts_half_plus : ∏ x y : Dcuts, Dcuts_half (Dcuts_plus x y) = Dcuts_plus (Dcuts_half x) (Dcuts_half y).
proof: Proof. intros x y. apply Dcuts_eq_is_eq. intros r ; split. - apply hinhfun ; apply sumofmaps ; [apply sumofmaps ; [intros Xr | intros Yr] | intros xy ]. + left. left. exact Xr. + left. right. exact Yr. + right. exists (pr1 (pr1 xy) / 2%NRat,, pr2 (pr1 xy)/2%NRat). unfold Dcuts_half_val ; simpl ; repeat split. * unfold divNonnegativeRationals. rewrite <- isrdistr_mult_plusNonnegativeRationals. pattern r at 1 ; rewrite (NQhalf_double r) ; unfold divNonnegativeRationals ; rewrite <- isrdistr_mult_plusNonnegativeRationals. apply (maponpaths (λ x, x * _)), (pr1 (pr2 xy)). * unfold Dcuts_half_val ; rewrite <- NQhalf_double. exact (pr1 (pr2 (pr2 xy))). * unfold Dcuts_half_val ; rewrite <- NQhalf_double. exact (pr2 (pr2 (pr2 xy))). - apply hinhfun ; apply sumofmaps ; [apply sumofmaps ; [intros Xr | intros Yr] | intros xy ; rewrite (pr1 (pr2 xy))]. + left. left. exact Xr. + left. right. exact Yr. + right. exists (pr1 (pr1 xy) + pr1 (pr1 xy),, pr2 (pr1 xy) + pr2 (pr1 xy)). simpl ; repeat split. * rewrite !isassoc_plusNonnegativeRationals. apply maponpaths. rewrite iscomm_plusNonnegativeRationals, isassoc_plusNonnegativeRationals. reflexivity. * exact (pr1 (pr2 (pr2 xy))). * exact (pr2 (pr2 (pr2 xy))). 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