proposition: Lemma ispositive_NQhalf : ∏ x, (0 < x) <-> (0 < x / 2).
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.RealNumbers.Sets UniMath.RealNumbers.Fields UniMath.Algebra.DivisionRig UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim