Lemma plusNonnegativeReals_eqcompat_l : ∏ x y z: NonnegativeReals, (y + x = z + x) <-> (y = z). Proof. intros x y z ; split. - intro H ; apply isantisymm_leNonnegativeReals ; split. + apply_pr2 (plusNonnegativeReals_lecompat_l x). rewrite H ; refine (isrefl_leNonnegativeReals _). + apply_pr2 (plusNonnegativeReals_lecompat_l x). rewrite H ; refine (isrefl_leNonnegativeReals _). - now intros ->. Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.