Lemma ispositive_invNonnegativeRationals : ∏ x, (0 < x) <-> (0 < / x). 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.
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.