proposition: Lemma ispositive_invNonnegativeRationals : ∏ x, (0 < x) <-> (0 < / x).
proof: Proof. intros x. split ; intro Hx. - apply_pr2 (multNonnegativeRationals_ltcompat_l x). + exact Hx. + rewrite israbsorb_zero_multNonnegativeRationals, isrinv_NonnegativeRationals. * exact ispositive_oneNonnegativeRationals. * apply NonnegativeRationals_neq0_gt0 ; intros Hx0. revert Hx ; rewrite Hx0. now apply isirrefl_ltNonnegativeRationals. - apply_pr2 (multNonnegativeRationals_ltcompat_r (/ x)). + exact Hx. + rewrite islabsorb_zero_multNonnegativeRationals, isrinv_NonnegativeRationals. * exact ispositive_oneNonnegativeRationals. * apply NonnegativeRationals_neq0_gt0 ; intros Hx0. revert Hx ; rewrite Hx0. unfold invNonnegativeRationals, hnnq_inv. generalize (hqlehchoice 0%hq (pr1 0) (pr2 0)). apply (coprod_rect (λ _, _ → _)) ; intros Hx. ** apply fromempty ; revert Hx. now apply isirreflhqlth. ** now apply isirrefl_ltNonnegativeRationals. 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