proposition: Lemma iscomm_Dcuts_mult : iscomm Dcuts_mult.
proof: 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.
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