Lemma islapbinop_plus : islapbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op1. 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.
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.