Lemma Dcuts_mult_ltcompat_l : ∏ x y z: Dcuts, (0 < x) -> (y < z) -> (Dcuts_mult y x < Dcuts_mult z x). Proof. intros X Y Z. apply hinhuniv2 ; intros x r. generalize (is_Dcuts_bot _ _ (pr2 (pr2 x)) _ (isnonnegative_NonnegativeRationals _)) ; clear x ; intro X0. induction (eq0orgt0NonnegativeRationals (pr1 r)) as [Hr0 | Hr0]. - apply hinhpr ; exists 0%NRat ; split. + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros yx. apply (pr1 (pr2 r)). rewrite Hr0. apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 yx))). now apply isnonnegative_NonnegativeRationals. + apply hinhpr ; exists (pr1 r,,0%NRat) ; simpl ; repeat split. * now rewrite israbsorb_zero_multNonnegativeRationals. * exact (pr2 (pr2 r)). * exact X0. - generalize (is_Dcuts_open _ _ X0) ; apply hinhuniv ; intros x. generalize (is_Dcuts_open _ _ (pr2 (pr2 r))) ; apply hinhuniv ; intros r'. set (c := ((pr1 r' - pr1 r) / pr1 r * pr1 x)%NRat). assert (Hc0 : (0 < c)%NRat). { unfold c. apply ispositive_multNonnegativeRationals. - apply ispositive_divNonnegativeRationals. + apply ispositive_minusNonnegativeRationals. exact (pr2 (pr2 r')). + exact Hr0. - exact (pr2 (pr2 x)). } generalize (Dcuts_def_corr_not_empty _ X0 (is_Dcuts_corr _) _ Hc0) ; apply hinhfun ; intros x'. exists (pr1 r * (NQmax (pr1 x) (pr1 x') + c))%NRat ; split. + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros yx. generalize (pr1 (pr2 yx)) ; apply gtNonnegativeRationals_noteq. apply multNonnegativeRationals_ltcompat. * apply (Dcuts_finite Y). ** exact (pr1 (pr2 r)). ** exact (pr1 (pr2 (pr2 yx))). * apply (Dcuts_finite X). ** intro ; apply (pr2 (pr2 x')). apply is_Dcuts_bot with (1 := X1). apply plusNonnegativeRationals_lecompat_r. now apply NQmax_le_r. ** exact (pr2 (pr2 (pr2 yx))). + apply hinhpr ; exists (pr1 r',,((pr1 r * (NQmax (pr1 x) (pr1 x') + c)) / (pr1 r'))%NRat) ; simpl ; repeat split. * rewrite multdivNonnegativeRationals. { reflexivity. } apply istrans_le_lt_ltNonnegativeRationals with (pr1 r). ** exact (isnonnegative_NonnegativeRationals _). ** exact (pr2 (pr2 r')). * exact (pr1 (pr2 r')). * apply (is_Dcuts_bot _ (NQmax (pr1 x) (pr1 x'))%NRat). ** apply NQmax_case. { exact (pr1 (pr2 x)). } exact (pr1 (pr2 x')). ** apply multNonnegativeRationals_lecompat_r' with (pr1 r'). *** apply istrans_le_lt_ltNonnegativeRationals with (pr1 r). { exact (isnonnegative_NonnegativeRationals _). } exact (pr2 (pr2 r')). *** unfold divNonnegativeRationals. rewrite !isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, isrunit_oneNonnegativeRationals, isldistr_mult_plusNonnegativeRationals, iscomm_multNonnegativeRationals. **** apply (minusNonnegativeRationals_lecompat_l' (NQmax (pr1 x) (pr1 x') * pr1 r)%NRat). { apply multNonnegativeRationals_lecompat_l, lt_leNonnegativeRationals. exact (pr2 (pr2 r')). } rewrite plusNonnegativeRationals_minus_l. rewrite <- isldistr_mult_minusNonnegativeRationals, iscomm_multNonnegativeRationals. apply multNonnegativeRationals_lecompat_r' with (/ pr1 r). { now apply ispositive_invNonnegativeRationals. } rewrite !isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals, iscomm_multNonnegativeRationals. { apply multNonnegativeRationals_lecompat_l. now apply NQmax_le_l. } exact Hr0. **** apply istrans_ltNonnegativeRationals with (pr1 r). { exact Hr0. } exact (pr2 (pr2 r')). 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.