Lemma hr_ap_lt : ∏ X Y : hr_commring, hr_ap_rel X Y <-> (hr_lt_rel X Y) ⨿ (hr_lt_rel Y X). Proof. intros X Y. rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y). split ; intro Hap. - apply_pr2_in NR_to_hr_ap Hap. revert Hap. apply sumofmaps ; intros Hlt. + now left ; apply NR_to_hr_lt. + now right ; apply NR_to_hr_lt. - apply NR_to_hr_ap. revert Hap ; apply sumofmaps ; intros Hlt. + now left ; apply_pr2 NR_to_hr_lt. + now right ; apply_pr2 NR_to_hr_lt. 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.