proposition: Lemma hr_ap_0_1 : isnonzeroCR hr_commring (hr_ap_rel,, istightap_hr_ap).
proof: 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.
imports: UniMath.Algebra.Groups UniMath.Foundations.Preamble UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals