Lemma iscomm_Dcuts_plus : iscomm Dcuts_plus. 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.
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.