proposition: Lemma ispositive_multNonnegativeReals : ∏ x y : NonnegativeReals, 0 < x ∧ 0 < y <-> 0 < x * y.
proof: Proof. intros x y. split. - intros H. rewrite <- (islabsorb_zero_multNonnegativeReals y). apply multNonnegativeReals_ltcompat_l. + apply (pr2 H). + apply (pr1 H). - intros H ; split. + eapply multNonnegativeReals_ltcompat_l'. rewrite islabsorb_zero_multNonnegativeReals. exact H. + eapply multNonnegativeReals_ltcompat_r'. rewrite israbsorb_zero_multNonnegativeReals. exact H. Qed.
imports: UniMath.Algebra.Groups UniMath.Foundations.Preamble UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals