Lemma invNonnegativeRationals_correct : ∏ (x : NonnegativeRationals) (Hx : 0 < x), / x = Rationals_to_NonnegativeRationals (/ pr1 x)%hq (hqlthtoleh _ _ (hqinv_gt0 _ Hx)). Proof. intros x Hx0. apply subtypePath_prop. unfold invNonnegativeRationals, hnnq_inv. generalize (hqlehchoice 0%hq (pr1 x) (pr2 x)). apply coprod_rect ; [intros Hlt | intros Heq]. - reflexivity. - apply fromempty ; generalize Hx0. change x with (pr1 x,,pr2 x). generalize (pr2 x). rewrite <- Heq ; intro. exact (isirreflhqlth 0%hq). 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.