Lemma iscomm_Dcuts_mult : iscomm Dcuts_mult. Proof. intros x y. apply Dcuts_eq_is_eq ; intro r ; split. - apply hinhfun. intros xy. exists (pr2 (pr1 xy),, pr1 (pr1 xy)) ; repeat split. + rewrite iscomm_multNonnegativeRationals. exact (pr1 (pr2 xy)). + exact (pr2 (pr2 (pr2 xy))). + exact (pr1 (pr2 (pr2 xy))). - apply hinhfun ; intros xy. exists (pr2 (pr1 xy),, pr1 (pr1 xy)) ; repeat split. + rewrite iscomm_multNonnegativeRationals. exact (pr1 (pr2 xy)). + exact (pr2 (pr2 (pr2 xy))). + exact (pr1 (pr2 (pr2 xy))). 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.