Lemma ispositive_Dcuts_half: ∏ x : Dcuts, (0 < x) <-> (0 < Dcuts_half x). Proof. intros. rewrite Dcuts_half_correct. pattern 0 at 2 ; rewrite <- (islabsorb_Dcuts_mult_zero (Dcuts_inv Dcuts_two Dcuts_two_ap_zero)). split. - intro Hx0. apply Dcuts_mult_ltcompat_l. + apply Dcuts_mult_ltcompat_l' with Dcuts_two. rewrite islabsorb_Dcuts_mult_zero, islinv_Dcuts_inv. unfold Dcuts_zero, Dcuts_one. apply (pr2 (isapfun_NonnegativeRationals_to_Dcuts_aux 0%NRat 1%NRat)). now apply ispositive_oneNonnegativeRationals. + exact Hx0. - now apply Dcuts_mult_ltcompat_l'. 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.