Lemma plusNonnegativeReals_apcompat_l : ∏ x y z: NonnegativeReals, (y ≠ z) <-> (y + x ≠ z + x). Proof. intros a b c. split. - intro H. apply ap_ltNonnegativeReals. apply_pr2_in ap_ltNonnegativeReals H. induction H as [H | H]. + left ; now apply plusNonnegativeReals_ltcompat_l. + right ; now apply plusNonnegativeReals_ltcompat_l. - now apply islapbinop_Dcuts_plus. 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.