Lemma islapbinop_mult : islapbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op2. Proof. intros X Y Z. unfold tightapSet_rel ; simpl pr1. rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y), <- (hr_to_NR_bij Z), !NR_to_hr_mult. intros Hap. apply_pr2_in NR_to_hr_ap Hap ; simpl in Hap. cut (∏ Y Z, (pr1 (hr_to_NR Z) * pr1 (hr_to_NR X) + pr2 (hr_to_NR Z) * pr2 (hr_to_NR X) + (pr1 (hr_to_NR Y) * pr2 (hr_to_NR X) + pr2 (hr_to_NR Y) * pr1 (hr_to_NR X))) = (pr1 (hr_to_NR Z) + pr2 (hr_to_NR Y)) * pr1 (hr_to_NR X) + (pr2 (hr_to_NR Z) + pr1 (hr_to_NR Y)) * pr2 (hr_to_NR X)). - intro H ; simpl in H,Hap ; rewrite !H in Hap ; clear H. apply ap_plusNonnegativeReals in Hap. apply NR_to_hr_ap. revert Hap ; apply hinhuniv ; apply sumofmaps ; intros Hap. + apply ap_multNonnegativeReals in Hap. revert Hap ; apply hinhuniv ; apply sumofmaps ; intros Hap. * exact Hap. * now eapply fromempty, (isirrefl_apNonnegativeReals _), Hap . + apply ap_multNonnegativeReals in Hap. revert Hap ; apply hinhuniv ; apply sumofmaps ; intros Hap. * rewrite (iscomm_plusNonnegativeReals (pr1 (hr_to_NR Z))), iscomm_plusNonnegativeReals. now apply issymm_apNonnegativeReals, Hap. * now eapply fromempty, (isirrefl_apNonnegativeReals _), Hap. - clear ; intros Y Z. rewrite !isrdistr_plus_multNonnegativeReals. rewrite !isassoc_plusNonnegativeReals. apply_pr2 plusNonnegativeReals_eqcompat_r. do 2 rewrite iscomm_plusNonnegativeReals, !isassoc_plusNonnegativeReals. reflexivity. 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.