Lemma NQhalf_double : ∏ x, x = x / 2 + x / 2. Proof. intros x. change x with (pr1 x,,pr2 x). generalize (pr1 x) (pr2 x) ; clear x ; intros x Hx. unfold divNonnegativeRationals, invNonnegativeRationals, hnnq_inv, twoNonnegativeRationals, Rationals_to_NonnegativeRationals ; simpl pr1 ; simpl pr2. generalize (hqlehchoice 0%hq 2%hq (hqlthtoleh 0%hq 2%hq hq2_gt0)) ; apply coprod_rect ; intros H2. - apply subtypePath_prop ; simpl pr1. rewrite !(hqmultcomm x), <- hqldistr, hqmultcomm. apply hqplusdiv2. - apply fromempty ; generalize hq2_gt0. rewrite H2. now apply (isirreflhqlth 2%hq). Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.Fields. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim.