Lemma hr_ap_0_1 : isnonzeroCR hr_commring (hr_ap_rel,, istightap_hr_ap). Proof. change (hr_ap_rel 1%ring 0%ring). rewrite <- (hr_to_NR_bij 1%ring), <- (hr_to_NR_bij 0%ring), hr_to_NR_one, hr_to_NR_zero. apply NR_to_hr_ap. rewrite !isrunit_zero_plusNonnegativeReals. apply isnonzeroNonnegativeReals. Qed.
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.