Lemma ispositive_NQhalf : ∏ x, (0 < x) <-> (0 < x / 2). Proof. intro x. split ; intro Hx. - apply_pr2 (multNonnegativeRationals_ltcompat_r 2). + now apply ispositive_twoNonnegativeRationals. + unfold divNonnegativeRationals ; rewrite isassoc_multNonnegativeRationals, islabsorb_zero_multNonnegativeRationals. rewrite islinv_NonnegativeRationals. * now rewrite isrunit_oneNonnegativeRationals. * now apply ispositive_twoNonnegativeRationals. - apply_pr2 (multNonnegativeRationals_ltcompat_r (/2)). + apply (pr1 (ispositive_invNonnegativeRationals _)). now apply ispositive_twoNonnegativeRationals. + rewrite islabsorb_zero_multNonnegativeRationals. exact Hx. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.Fields. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim.