proposition: Lemma ispositive_Dcuts_half: ∏ x : Dcuts, (0 < x) <-> (0 < Dcuts_half x).
proof: 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.
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