Lemma Dcuts_mult_corr_aux : Dcuts_def_corr Dcuts_mult_val. Proof. intros c Hc0. apply ispositive_NQhalf in Hc0. generalize (Y_corr _ Hc0). apply hinhuniv ; apply sumofmaps ; intros Hy. - apply hinhpr ; left. unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros xy. generalize (pr1 (pr2 xy)). apply gtNonnegativeRationals_noteq. pattern c at 1 ; rewrite <- (islunit_oneNonnegativeRationals c). apply multNonnegativeRationals_ltcompat. + apply notge_ltNonnegativeRationals ; intro H. apply Hx1, X_bot with (1 := pr1 (pr2 (pr2 xy))). exact H. + apply notge_ltNonnegativeRationals ; intro H. apply Hy, Y_bot with (1 := pr2 (pr2 (pr2 xy))). apply istrans_leNonnegativeRationals with (2 := H). pattern c at 2 ; rewrite (NQhalf_double c). now apply plusNonnegativeRationals_le_r. - rename Hy into y. assert (Hq1 : (0 < pr1 y + c / 2)%NRat). { apply istrans_lt_le_ltNonnegativeRationals with (c / 2)%NRat. { exact Hc0. } now apply plusNonnegativeRationals_le_l. } set (cx := ((c / 2) / (pr1 y + (c / 2)))%NRat). assert (Hcx0 : (0 < cx)%NRat) by (now apply ispositive_divNonnegativeRationals). generalize (X_corr _ Hcx0) ; apply hinhfun ; apply sumofmaps ; intros H. + left. unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros xy. generalize (pr1 (pr2 xy)). apply gtNonnegativeRationals_noteq. apply istrans_ltNonnegativeRationals with (c / 2)%NRat. * rewrite <- (multdivNonnegativeRationals (c / 2)%NRat (pr1 y + (c / 2)%NRat)). ** rewrite iscomm_multNonnegativeRationals. apply multNonnegativeRationals_ltcompat. *** apply notge_ltNonnegativeRationals ; intro H0. apply (pr2 (pr2 y)), Y_bot with (1 := pr2 (pr2 (pr2 xy))). exact H0. *** apply notge_ltNonnegativeRationals ; intro H0. apply H, X_bot with (1 := pr1 (pr2 (pr2 xy))). exact H0. ** exact Hq1. * rewrite <- (islunit_zeroNonnegativeRationals (c / 2)%NRat). pattern c at 2 ; rewrite (NQhalf_double c). now apply plusNonnegativeRationals_ltcompat_r. + right. rename H into x. exists (pr1 x * pr1 y) ; repeat split. * apply hinhpr. exists (pr1 x,, pr1 y) ; simpl ; repeat split. ** exact (pr1 (pr2 x)). ** exact (pr1 (pr2 y)). * unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros xy. generalize (pr1 (pr2 xy)). apply gtNonnegativeRationals_noteq. apply istrans_lt_le_ltNonnegativeRationals with ((pr1 x + cx)* (pr1 y + (c / 2)%NRat)). ** apply multNonnegativeRationals_ltcompat. *** apply notge_ltNonnegativeRationals. intros H ; apply (pr2 (pr2 x)), X_bot with (1 := pr1 (pr2 (pr2 xy))). exact H. *** apply notge_ltNonnegativeRationals. intros H ; apply (pr2 (pr2 y)), Y_bot with (1 := pr2 (pr2 (pr2 xy))). exact H. ** rewrite isrdistr_mult_plusNonnegativeRationals, (iscomm_multNonnegativeRationals cx). unfold cx ; rewrite multdivNonnegativeRationals. *** pattern c at 3; rewrite (NQhalf_double c), <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_r. rewrite isldistr_mult_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. rewrite iscomm_multNonnegativeRationals. apply multNonnegativeRationals_le1_r. apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals. intro H ; apply Hx1. now apply X_bot with (1 := pr1 (pr2 x)). *** exact Hq1. 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.