Lemma ispositive_multNonnegativeReals : ∏ x y : NonnegativeReals, 0 < x ∧ 0 < y <-> 0 < x * y. 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.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.