Definition minusNonnegativeReals_plus_r : ∏ x y z : NonnegativeReals, z <= y -> x = y - z -> y = x + z := Dcuts_minus_plus_r.
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.