proposition: Lemma NQhalf_double : ∏ x, x = x / 2 + x / 2.
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.RealNumbers.Sets UniMath.RealNumbers.Fields UniMath.Algebra.DivisionRig UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim