Lemma isldistr_mult_minusNonnegativeRationals: ∏ x y z : NonnegativeRationals, z * (x - y) = z * x - z * y. Proof. intros x y z. generalize (isdecrel_leNonnegativeRationals x y) ; apply sumofmaps ; [ intros Hle | intros Hlt]. - rewrite !minusNonnegativeRationals_eq_zero. + now apply israbsorb_zero_multNonnegativeRationals. + now apply multNonnegativeRationals_lecompat_l, Hle. + exact Hle. - apply notge_ltNonnegativeRationals in Hlt ; apply lt_leNonnegativeRationals in Hlt. apply plusNonnegativeRationals_eqcompat_r with (z * y). rewrite <- isldistr_mult_plusNonnegativeRationals. rewrite !minusNonnegativeRationals_plus_r. + reflexivity. + now apply multNonnegativeRationals_lecompat_l, Hlt. + exact Hlt. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.Fields. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim.