proposition: Lemma Dcuts_inv_corr : Dcuts_def_corr (Dcuts_inv_val X).
proof: Proof. generalize (X_open _ X_0) ; apply (hinhuniv (P := make_hProp _ (isaprop_Dcuts_def_corr _))) ; intros x. set (Y := Dcuts_NQmult_val (/ (pr1 x))%NRat X). assert (Y_1 : Y 1%NRat). { unfold Y ; apply hinhpr ; exists (pr1 x) ; split. - apply pathsinv0, islinv_NonnegativeRationals. exact (pr2 (pr2 x)). - exact (pr1 (pr2 x)). } assert (Heq : Dcuts_inv_val X = Dcuts_NQmult_val (/(pr1 x))%NRat (Dcuts_inv_val Y)). { apply funextfun ; intro r. apply hPropUnivalence. - apply hinhfun ; intros l. exists (pr1 x * r) ; split. + rewrite <- isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, islunit_oneNonnegativeRationals. * reflexivity. * exact (pr2 (pr2 x)). + apply hinhpr. exists (pr1 l) ; repeat split. * intros q ; unfold Y. apply hinhuniv ; intros s. rewrite (pr1 (pr2 s)). rewrite (iscomm_multNonnegativeRationals (pr1 x)), <- isassoc_multNonnegativeRationals. rewrite iscomm_multNonnegativeRationals, !isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals, iscomm_multNonnegativeRationals. ** apply (pr1 (pr2 l)). exact (pr2 (pr2 s)). ** exact (pr2 (pr2 x)). * exact (pr1 (pr2 (pr2 l))). * exact (pr2 (pr2 (pr2 l))). - apply hinhuniv. intros q. rewrite (pr1 (pr2 q)). generalize (pr2 (pr2 q)). apply hinhfun ; intros l. exists (pr1 l) ; repeat split. + intros s Xs. rewrite (iscomm_multNonnegativeRationals (/ pr1 x)%NRat), isassoc_multNonnegativeRationals. apply (pr1 (pr2 l)). unfold Y ; apply hinhpr. now exists s. + exact (pr1 (pr2 (pr2 l))). + exact (pr2 (pr2 (pr2 l))). } rewrite Heq. apply Dcuts_NQmult_corr. - apply ispositive_invNonnegativeRationals. exact (pr2 (pr2 x)). - now apply Dcuts_inv_bot. - apply Dcuts_inv_corr_aux. + now unfold Y ; apply Dcuts_NQmult_bot. + unfold Y ; apply Dcuts_NQmult_corr. * apply ispositive_invNonnegativeRationals. exact (pr2 (pr2 x)). * exact X_bot. * exact X_corr. + apply hinhpr ; exists 0%NRat ; split. * now rewrite israbsorb_zero_multNonnegativeRationals. * exact X_0. + exact Y_1. Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals