Lemma Dcuts_mult_corr : Dcuts_def_corr (Dcuts_mult_val X Y). Proof. intros c Hc. generalize (X_corr 1%NRat ispositive_oneNonnegativeRationals). apply hinhuniv ; apply sumofmaps ; [ intros Hx1 | intros x]. - now apply Dcuts_mult_corr_aux. - assert (Hx1 : (0 < pr1 x + 1)%NRat). { apply istrans_lt_le_ltNonnegativeRationals with (1 := ispositive_oneNonnegativeRationals). apply plusNonnegativeRationals_le_l. } assert (Heq : Dcuts_mult_val X Y = (Dcuts_NQmult_val (pr1 x + 1%NRat) (Dcuts_mult_val (Dcuts_NQmult_val (/ (pr1 x + 1))%NRat X) Y))). { apply funextfun ; intro r. apply hPropUnivalence. - apply hinhfun. intros xy. exists (r / (pr1 x + 1))%NRat ; split. + now rewrite multdivNonnegativeRationals. + apply hinhpr. exists (pr1 (pr1 xy) / (pr1 x + 1%NRat),,pr2 (pr1 xy))%NRat ; simpl ; repeat split. * unfold divNonnegativeRationals. rewrite isassoc_multNonnegativeRationals, (iscomm_multNonnegativeRationals (/ (pr1 x + 1))%NRat). rewrite <- isassoc_multNonnegativeRationals. now pattern r at 1 ; rewrite (pr1 (pr2 xy)). * apply hinhpr. exists (pr1 (pr1 xy)) ; split. ** now apply iscomm_multNonnegativeRationals. ** exact (pr1 (pr2 (pr2 xy))). * exact (pr2 (pr2 (pr2 xy))). - apply hinhuniv. intros rx. generalize (pr2 (pr2 rx)) ; apply hinhuniv. intros xy. generalize (pr1 (pr2 (pr2 xy))) ; apply hinhfun ; intros rx'. rewrite (pr1 (pr2 rx)), (pr1 (pr2 xy)), (pr1 (pr2 rx')). exists (pr1 rx',,pr2 (pr1 xy)) ; repeat split. + now rewrite <- !isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, islunit_oneNonnegativeRationals. + exact (pr2 (pr2 rx')). + exact (pr2 (pr2 (pr2 xy))). } rewrite Heq. revert c Hc. apply Dcuts_NQmult_corr. + exact Hx1. + apply Dcuts_mult_bot, Y_bot. now apply Dcuts_NQmult_bot. + apply Dcuts_mult_corr_aux. * now apply Dcuts_NQmult_bot. * apply Dcuts_NQmult_corr. ** now apply ispositive_invNonnegativeRationals. ** exact X_bot. ** exact X_corr. * exact Y_bot. * exact Y_corr. * unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros rx. apply (pr2 (pr2 x)), X_bot with (1 := pr2 (pr2 rx)). rewrite <- (isrunit_oneNonnegativeRationals (pr1 x + 1%NRat)). pattern 1%NRat at 2; rewrite (pr1 (pr2 rx)), <- isassoc_multNonnegativeRationals. rewrite isrinv_NonnegativeRationals, islunit_oneNonnegativeRationals. ** now apply isrefl_leNonnegativeRationals. ** exact Hx1. Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.