proposition: Lemma invNonnegativeRationals_correct : ∏ (x : NonnegativeRationals) (Hx : 0 < x), / x = Rationals_to_NonnegativeRationals (/ pr1 x)%hq (hqlthtoleh _ _ (hqinv_gt0 _ Hx)).
proof: 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.
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