Lemma hr_abs_mult : ∏ x y : hr_ConstructiveField, hr_abs (x * y)%ring = hr_abs x * hr_abs y. Proof. intros x y. pattern x at 1 ; rewrite <- (hr_to_NR_bij x) ; pattern y at 1 ; rewrite <- (hr_to_NR_bij y). rewrite NR_to_hr_mult. change (pr1 (hr_to_NR x)) with (hr_to_NRpos x) ; change (pr1 (hr_to_NR y)) with (hr_to_NRpos y) ; change (pr2 (hr_to_NR x)) with (hr_to_NRneg x) ; change (pr2 (hr_to_NR y)) with (hr_to_NRneg y). rewrite <- !max_plusNonnegativeReals. - unfold hr_abs. rewrite hr_to_NRpos_NR_to_hr_std, hr_to_NRneg_NR_to_hr_std ; simpl. + rewrite isldistr_max_multNonnegativeReals, !isrdistr_max_multNonnegativeReals. rewrite !isassoc_maxNonnegativeReals. apply maponpaths. rewrite iscomm_maxNonnegativeReals, !isassoc_maxNonnegativeReals. rewrite iscomm_maxNonnegativeReals, !isassoc_maxNonnegativeReals. apply maponpaths. apply iscomm_maxNonnegativeReals. + intros H. apply maxNonnegativeReals_lt' in H. apply le0_NonnegativeReals. revert H ; apply hinhuniv ; apply sumofmaps ; intros H ; apply_pr2_in ispositive_multNonnegativeReals H ; apply maxNonnegativeReals_le ; apply_pr2 le0_NonnegativeReals. * now rewrite (hr_to_NRposneg_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals. * now rewrite (hr_to_NRposneg_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals. * now rewrite (hr_to_NRnegpos_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals. * now rewrite (hr_to_NRnegpos_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals. + intros H. apply maxNonnegativeReals_lt' in H. apply le0_NonnegativeReals. revert H ; apply hinhuniv ; apply sumofmaps ; intros H ; apply_pr2_in ispositive_multNonnegativeReals H ; apply maxNonnegativeReals_le ; apply_pr2 le0_NonnegativeReals. * now rewrite (hr_to_NRposneg_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals. * now rewrite (hr_to_NRposneg_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals. * now rewrite (hr_to_NRnegpos_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals. * now rewrite (hr_to_NRnegpos_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals. - intros H. apply_pr2_in ispositive_multNonnegativeReals H. rewrite hr_to_NRposneg_zero. + apply islabsorb_zero_multNonnegativeReals. + exact (pr1 H). - intros H. apply_pr2_in ispositive_multNonnegativeReals H. rewrite hr_to_NRposneg_zero. + apply islabsorb_zero_multNonnegativeReals. + exact (pr1 H). 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.