proposition: Lemma hqinv_gt0 (x : hq) : 0 < x → 0 < / x.
proof: Proof. unfold hqlth. intros Hx. apply hqgthandmultlinv with x. - exact Hx. - rewrite hqmultx0. rewrite hqisrinvmultinv. + exact hq1_gt0. + apply hqgth_hqneq. exact Hx. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean