proposition: Lemma hr_ap_lt : ∏ X Y : hr_commring, hr_ap_rel X Y <-> (hr_lt_rel X Y) ⨿ (hr_lt_rel Y X).
proof: 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.
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