proposition: Lemma iscomm_Dcuts_plus : iscomm Dcuts_plus.
proof: Proof. assert (H : ∏ x y, ∏ x0 : NonnegativeRationals, x0 ∈ Dcuts_plus x y -> x0 ∈ Dcuts_plus y x). { intros x y r. apply hinhuniv, sumofmaps ; simpl pr1. - apply sumofmaps ; intros Hr. + now apply hinhpr ; left ; right. + now apply hinhpr ; left ; left. - intros xy. apply hinhpr ; right ; exists (pr2 (pr1 xy),, pr1 (pr1 xy)). repeat split. + pattern r at 1 ; rewrite (pr1 (pr2 xy)). apply iscomm_plusNonnegativeRationals. + exact (pr2 (pr2 (pr2 xy))). + exact (pr1 (pr2 (pr2 xy))). } intros x y. apply Dcuts_eq_is_eq ; intro r ; split. - now apply H. - now apply H. 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