proposition: Lemma Dcuts_min_carac_r : ∏ x y : Dcuts, y <= x -> Dcuts_min x y = y.
proof: Proof. intros x y Hxy. apply Dcuts_eq_is_eq ; intros r ; split. - intros Hr. exact (pr2 Hr). - intros Yr. split. + now simple refine (Hxy _ _). + exact Yr. 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