Lemma istightap_hr_ap : istightap hr_ap_rel. Proof. repeat split. - intros X Hap. rewrite <- (hr_to_NR_bij X) in Hap. apply_pr2_in NR_to_hr_ap Hap. revert Hap. now apply isirrefl_apNonnegativeReals. - intros X Y. rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y). intros Hap. apply NR_to_hr_ap. apply issymm_apNonnegativeReals. now apply_pr2 NR_to_hr_ap. - intros X Y Z Hap. apply hr_ap_lt in Hap. revert Hap ; apply sumofmaps ; intros Hlt. + apply (iscotrans_hr_lt X Y Z) in Hlt. revert Hlt ; apply hinhfun ; apply sumofmaps ; intros Hlt. * left ; apply_pr2 hr_ap_lt. now left. * right ; apply_pr2 hr_ap_lt. now left. + apply (iscotrans_hr_lt _ Y _) in Hlt. revert Hlt ; apply hinhfun ; apply sumofmaps ; intros Hlt. * right ; apply_pr2 hr_ap_lt. now right. * left ; apply_pr2 hr_ap_lt. now right. - intros X Y Hap. apply isantisymm_hr_le. + apply hr_notlt_le. intro Hlt ; apply Hap. apply_pr2 hr_ap_lt. now right. + apply hr_notlt_le. intro Hlt ; apply Hap. apply_pr2 hr_ap_lt. now left. 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.