Lemma Dcuts_NQmult_corr : Dcuts_def_corr Dcuts_NQmult_val. Proof. intros c Hc. assert (Hcx : (0 < c / x)%NRat) by (now apply ispositive_divNonnegativeRationals). generalize (Y_corr _ Hcx). apply hinhfun ; apply sumofmaps ; intros Hy. - left. unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros ry. generalize (pr1 (pr2 ry)). apply gtNonnegativeRationals_noteq. pattern c at 1 ; rewrite <- (multdivNonnegativeRationals c x). + apply (pr2 (lt_gtNonnegativeRationals _ _)). apply (multNonnegativeRationals_ltcompat_l x (pr1 ry) (c / x)%NRat Hx). apply notge_ltNonnegativeRationals. intro Hy' ; apply Hy. apply Y_bot with (pr1 ry). * exact (pr2 (pr2 ry)). * exact Hy'. + exact Hx. - right. rename Hy into q. exists (x * pr1 q). split. + apply hinhpr. exists (pr1 q). split. * reflexivity. * exact (pr1 (pr2 q)). + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros ry. generalize (pr1 (pr2 ry)). apply gtNonnegativeRationals_noteq. pattern c at 1; rewrite <- (multdivNonnegativeRationals c x), <-isldistr_mult_plusNonnegativeRationals. * apply (pr2 ( lt_gtNonnegativeRationals _ _)). apply (multNonnegativeRationals_ltcompat_l x (pr1 ry) (pr1 q + c / x)%NRat Hx). apply notge_ltNonnegativeRationals. intro Hy' ; apply (pr2 (pr2 q)). apply Y_bot with (pr1 ry). ** exact (pr2 (pr2 ry)). ** exact Hy'. * exact Hx. 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.