Lemma nat_to_hr_S : ∏ n : nat, nat_to_hr (S n) = (1 + nat_to_hr n)%ring. Proof. intros n. unfold nat_to_hr. rewrite nat_to_NonnegativeReals_Sn, iscomm_plusNonnegativeReals. rewrite <- (hr_to_NR_bij 1%ring), hr_to_NR_one, NR_to_hr_plus. rewrite !isrunit_zero_plusNonnegativeReals. reflexivity. 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.