proposition: Lemma plusNonnegativeReals_apcompat_l : ∏ x y z: NonnegativeReals, (y ≠ z) <-> (y + x ≠ z + x).
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals