proposition: Lemma islapbinop_plus : islapbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op1.
proof: Proof. intros X Y Z. unfold tightapSet_rel ; simpl pr1. intro Hap. apply_pr2 hr_ap_lt. apply hr_ap_lt in Hap. revert Hap ; apply sumofmaps ; intros Hlt. - left. apply_pr2 (hr_plus_ltcompat_l X). exact Hlt. - right. apply_pr2 (hr_plus_ltcompat_l X). exact Hlt. 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