Lemma hqinv_gt0 (x : hq) : 0 < x → 0 < / x. Proof. unfold hqlth. intros Hx. apply hqgthandmultlinv with x. - exact Hx. - rewrite hqmultx0. rewrite hqisrinvmultinv. + exact hq1_gt0. + apply hqgth_hqneq. exact Hx. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.