proposition: Lemma istightap_hr_ap : istightap hr_ap_rel.
proof: 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.
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