proposition: Lemma isldistr_mult_minusNonnegativeRationals: ∏ x y z : NonnegativeRationals, z * (x - y) = z * x - z * y.
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.RealNumbers.Sets UniMath.RealNumbers.Fields UniMath.Algebra.DivisionRig UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim