proposition: Lemma islapbinop_mult : islapbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op2.
proof: 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.
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