Lemma hqlth_between : ∏ x y : hq, x < y -> total2 (λ z, (x < z) × (z < y)). Proof. assert (H0 : / 2 > 0). { apply hqgthandmultlinv with 2. - apply hq2_gt0. - rewrite hqisrinvmultinv, hqmultx0. + now apply hq1_gt0. + now apply hqgth_hqneq, hq2_gt0. } intros x y Hlt. exists ((x + y) / 2). split. - pattern x at 1. rewrite (hqplusdiv2 x). unfold hqdiv. apply (hqlthandmultr _ _ (/ 2)). + exact H0. + now apply (hqlthandplusl _ _ x Hlt). - pattern y at 2. rewrite (hqplusdiv2 y). unfold hqdiv. apply (hqlthandmultr _ _ (/ 2)). + exact H0. + now apply (hqlthandplusr _ _ y Hlt). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.