proposition: Lemma hqplusdiv2 : ∏ x : hq, x = (x + x) / 2.
proof: Proof. intros x. apply hqmultrcan with 2. - now apply hqgth_hqneq, hq2_gt0. - unfold hqdiv. rewrite hqmultassoc. rewrite (hqislinvmultinv 2). 2: now apply hqgth_hqneq, hq2_gt0. rewrite (hqmultr1 (x + x)). apply hqmult2r. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean