Definition hr_ConstructiveField : ConstructiveField. Proof. exists hr_commring. exists (_,,istightap_hr_ap). repeat split. - exact islapbinop_plus. - exact israpbinop_plus. - exact islapbinop_mult. - exact israpbinop_mult. - exact hr_ap_0_1. - exact hr_ex_inv. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.