Definition hnnq_set := carrier_subset (hqleh 0). Local Definition hnnq_set_to_hq (r : hnnq_set) : hq := pr1 r. Local Definition hq_to_hnnq_set (r : hq) (Hr : hqleh 0 r) : hnnq_set := r ,, Hr. Local Definition hnnq_zero: hnnq_set := hq_to_hnnq_set 0 (isreflhqleh 0). Local Definition hnnq_one: hnnq_set := hq_to_hnnq_set 1 (hqlthtoleh 0 1 hq1_gt0). Local Definition hnnq_plus: binop hnnq_set := λ x y : hnnq_set, hq_to_hnnq_set (pr1 x + pr1 y) (hq0lehandplus _ _ (pr2 x) (pr2 y)). Local Definition hnnq_minus: binop hnnq_set. Proof. intros x y. induction (hqgthorleh (pr1 x) (pr1 y)) as [H | _]. - exact (hq_to_hnnq_set (pr1 x - pr1 y) (hq0leminus _ _ (hqlthtoleh _ _ H))). - exact hnnq_zero. Defined.
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.