Library UniMath.RealNumbers.NonnegativeReals

Definition of Dedekind cuts for non-negative real numbers

Catherine Lelay. Sep. 2015

Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.Notations.

Require Import UniMath.RealNumbers.Sets.
Require Export UniMath.Algebra.ConstructiveStructures.
Require Import UniMath.RealNumbers.Prelim.
Require Import UniMath.RealNumbers.NonnegativeRationals.

Declare Scope Dcuts_scope.
Delimit Scope Dcuts_scope with Dcuts.
Local Open Scope NRat_scope.
Local Open Scope Dcuts_scope.
Local Open Scope tap_scope.

Definition of Dedekind cuts


Definition Dcuts_def_bot (X : hsubtype NonnegativeRationals) : UU :=
   x : NonnegativeRationals,
        X x y : NonnegativeRationals, y x X y.
Definition Dcuts_def_open (X : hsubtype NonnegativeRationals) : UU :=
   x : NonnegativeRationals,
        X x y : NonnegativeRationals, (X y) × (x < y).
Definition Dcuts_def_finite (X : hsubtype NonnegativeRationals) : hProp :=
   ub : NonnegativeRationals, ¬ (X ub).
Definition Dcuts_def_corr (X : hsubtype NonnegativeRationals) : UU :=
   r : NonnegativeRationals, 0 < r (¬ (X r)) q : NonnegativeRationals, (X q) × (¬ (X (q + r))).

Lemma Dcuts_def_corr_finite (X : hsubtype NonnegativeRationals) :
  Dcuts_def_corr X Dcuts_def_finite X.
Proof.
  intros Hx.
  specialize (Hx _ ispositive_oneNonnegativeRationals).
  revert Hx ; apply hinhuniv ; apply sumofmaps ; [intros Hx | intros x].
  - apply hinhpr.
     1 ; exact Hx.
  - apply hinhpr ; (pr1 x + 1) ; exact (pr2 (pr2 x)).
Qed.

Lemma Dcuts_def_corr_not_empty (X : hsubtype NonnegativeRationals) :
  X 0 Dcuts_def_corr X
   c : NonnegativeRationals,
    (0 < c)%NRat x : NonnegativeRationals, X x × ¬ X (x + c).
Proof.
  intros X0 Hx c Hc.
  generalize (Hx c Hc).
  apply hinhuniv ; apply sumofmaps ; [intros nXc | intros Hx' ].
  - apply hinhpr ; 0%NRat ; split.
    exact X0.
    rewrite islunit_zeroNonnegativeRationals.
    exact nXc.
  - apply hinhpr ; exact Hx'.
Qed.

Lemma isaprop_Dcuts_def_bot (X : hsubtype NonnegativeRationals) : isaprop (Dcuts_def_bot X).
Proof.
  repeat (apply impred_isaprop ; intro).
  now apply pr2.
Qed.
Lemma isaprop_Dcuts_def_open (X : hsubtype NonnegativeRationals) : isaprop (Dcuts_def_open X).
Proof.
  repeat (apply impred_isaprop ; intro).
  now apply pr2.
Qed.
Lemma isaprop_Dcuts_def_corr (X : hsubtype NonnegativeRationals) : isaprop (Dcuts_def_corr X).
Proof.
  repeat (apply impred_isaprop ; intro).
  now apply pr2.
Qed.

Lemma isaprop_Dcuts_hsubtype (X : hsubtype NonnegativeRationals) :
  isaprop (Dcuts_def_bot X × Dcuts_def_open X × Dcuts_def_corr X).
Proof.
  apply isofhleveldirprod, isofhleveldirprod.
  - exact (isaprop_Dcuts_def_bot X).
  - exact (isaprop_Dcuts_def_open X).
  - exact (isaprop_Dcuts_def_corr X).
Qed.

Definition Dcuts_hsubtype : hsubtype (hsubtype NonnegativeRationals) :=
  λ X : hsubtype NonnegativeRationals, make_hProp _ (isaprop_Dcuts_hsubtype X).
Lemma isaset_Dcuts : isaset (carrier Dcuts_hsubtype).
Proof.
  apply isasetsubset with pr1.
  apply isasethsubtype.
  apply isinclpr1.
  intro x.
  apply pr2.
Qed.
Definition Dcuts_set : hSet := make_hSet _ isaset_Dcuts.
Definition pr1Dcuts (x : Dcuts_set) : hsubtype NonnegativeRationals := pr1 x.
Declare Scope DC_scope.
Notation "x ∈ X" := (pr1Dcuts X x) (at level 70, no associativity) : DC_scope.

Local Open Scope DC_scope.

Lemma is_Dcuts_bot (X : Dcuts_set) : Dcuts_def_bot (pr1 X).
Proof.
  exact (pr1 (pr2 X)).
Qed.
Lemma is_Dcuts_open (X : Dcuts_set) : Dcuts_def_open (pr1 X).
Proof.
  exact (pr1 (pr2 (pr2 X))).
Qed.
Lemma is_Dcuts_corr (X : Dcuts_set) : Dcuts_def_corr (pr1 X).
Proof.
  exact (pr2 (pr2 (pr2 X))).
Qed.

Definition make_Dcuts (X : NonnegativeRationals hProp)
                    (Hbot : Dcuts_def_bot X)
                    (Hopen : Dcuts_def_open X)
                    (Herror : Dcuts_def_corr X) : Dcuts_set.
Proof.
   X ; repeat split.
  now apply Hbot.
  now apply Hopen.
  now apply Herror.
Defined.

Lemma Dcuts_finite :
   X : Dcuts_set, r : NonnegativeRationals,
    neg (r X) n : NonnegativeRationals, n X n < r.
Proof.
  intros X r Hr n Hn.
  apply notge_ltNonnegativeRationals ; intro Hn'.
  apply Hr.
  apply is_Dcuts_bot with n.
  exact Hn.
  exact Hn'.
Qed.

Dcuts is a effectively ordered set

Partial order on Dcuts

Definition Dcuts_le_rel : hrel Dcuts_set :=
  λ X Y : Dcuts_set,
          make_hProp ( x : NonnegativeRationals, x X x Y)
                    (impred_isaprop _ (λ _, isapropimpl _ _ (pr2 _))).

Lemma istrans_Dcuts_le_rel : istrans Dcuts_le_rel.
Proof.
  intros x y z Hxy Hyz r Xr.
  refine (Hyz _ _). now refine (Hxy _ _).
Qed.
Lemma isrefl_Dcuts_le_rel : isrefl Dcuts_le_rel.
Proof.
  now intros X x Xx.
Qed.

Lemma ispreorder_Dcuts_le_rel : ispreorder Dcuts_le_rel.
Proof.
  split.
  exact istrans_Dcuts_le_rel.
  exact isrefl_Dcuts_le_rel.
Qed.

Strict partial order on Dcuts

Definition Dcuts_lt_rel : hrel Dcuts_set :=
  λ (X Y : Dcuts_set),
     x : NonnegativeRationals, dirprod (neg (x X)) (x Y).

Lemma istrans_Dcuts_lt_rel : istrans Dcuts_lt_rel.
Proof.
  intros x y z.
  apply hinhfun2.
  intros r n.
   (pr1 r) ; split.
  exact (pr1 (pr2 r)).
  apply is_Dcuts_bot with (pr1 n).
  exact (pr2 (pr2 n)).
  apply lt_leNonnegativeRationals.
  apply Dcuts_finite with y.
  exact (pr1 (pr2 n)).
  exact (pr2 (pr2 r)).
Qed.
Lemma isirrefl_Dcuts_lt_rel : isirrefl Dcuts_lt_rel.
Proof.
  intros x.
  unfold neg ;
  apply (hinhuniv (P := make_hProp _ isapropempty)).
  intros r.
  apply (pr1 (pr2 r)).
  exact (pr2 (pr2 r)).
Qed.
Lemma iscotrans_Dcuts_lt_rel :
  iscotrans Dcuts_lt_rel.
Proof.
  intros x y z.
  apply hinhuniv ; intros r.
  generalize (is_Dcuts_open _ _ (pr2 (pr2 r))) ; apply hinhuniv ; intros r'.
  assert (Hr0 : 0%NRat < pr1 r' - pr1 r).
  { apply ispositive_minusNonnegativeRationals.
    exact (pr2 (pr2 r')). }
  generalize (is_Dcuts_corr y _ Hr0) ; apply hinhuniv ; apply sumofmaps ; [intros Yq | intros q].
  - apply squash_element ;
    right ; apply squash_element.
     (pr1 r') ; split.
    + intro H0 ; apply Yq.
      apply is_Dcuts_bot with (pr1 r').
      exact H0.
      now apply minusNonnegativeRationals_le.
    + exact (pr1 (pr2 r')).
  - generalize (isdecrel_leNonnegativeRationals (pr1 q + (pr1 r' - pr1 r)) (pr1 r')) ; apply sumofmaps ; intros Hdec.
    + apply hinhpr ; right ; apply hinhpr.
       (pr1 r') ; split.
      intro Yr' ; apply (pr2 (pr2 q)).
      apply is_Dcuts_bot with (pr1 r').
      exact Yr'.
      exact Hdec.
      exact (pr1 (pr2 r')).
    + apply hinhpr ; left ; apply hinhpr.
       (pr1 q) ; split.
      × intro Xq ; apply (pr1 (pr2 r)).
        apply is_Dcuts_bot with (pr1 q).
        exact Xq.
        apply notge_ltNonnegativeRationals in Hdec.
        apply (plusNonnegativeRationals_ltcompat_r (pr1 r)) in Hdec ;
          rewrite isassoc_plusNonnegativeRationals, minusNonnegativeRationals_plus_r, iscomm_plusNonnegativeRationals in Hdec.
        apply_pr2_in plusNonnegativeRationals_ltcompat_r Hdec.
        now apply lt_leNonnegativeRationals, Hdec.
        now apply lt_leNonnegativeRationals, (pr2 (pr2 r')).
      × exact (pr1 (pr2 q)).
Qed.

Lemma isstpo_Dcuts_lt_rel : isStrongOrder Dcuts_lt_rel.
Proof.
  repeat split.
  exact istrans_Dcuts_lt_rel.
  exact iscotrans_Dcuts_lt_rel.
  exact isirrefl_Dcuts_lt_rel.
Qed.

Effectively Ordered Set

Lemma Dcuts_lt_le_rel :
   x y : Dcuts_set, Dcuts_lt_rel x y Dcuts_le_rel x y.
Proof.
  intros x y ; apply hinhuniv ; intros r.
  intros n Xn.
  apply is_Dcuts_bot with (pr1 r).
  exact (pr2 (pr2 r)).
  apply lt_leNonnegativeRationals.
  apply Dcuts_finite with x.
  exact (pr1 (pr2 r)).
  exact Xn.
Qed.

Lemma Dcuts_le_ngt_rel :
   x y : Dcuts_set, ¬ Dcuts_lt_rel x y Dcuts_le_rel y x.
Proof.
  intros X Y.
  split.
  - intros Hnlt y Yy.
    generalize (is_Dcuts_open _ _ Yy) ; apply hinhuniv ; intros y'.
    generalize (pr1 (ispositive_minusNonnegativeRationals _ _) (pr2 (pr2 y'))) ; intros Hy.
    generalize (is_Dcuts_corr X _ Hy).
    apply hinhuniv.
    apply sumofmaps ; [intros nXc | ].
    + apply fromempty, Hnlt.
      apply hinhpr.
       (pr1 y') ; split.
      × intro Xy' ; apply nXc.
        apply is_Dcuts_bot with (1 := Xy').
        now apply minusNonnegativeRationals_le.
      × exact (pr1 (pr2 y')).
    + intros x.
      apply is_Dcuts_bot with (1 := pr1 (pr2 x)).
      apply notlt_geNonnegativeRationals ; intro H ; apply Hnlt.
      apply hinhpr.
       (pr1 x + (pr1 y' - y)) ; split.
      × exact (pr2 (pr2 x)).
      × apply is_Dcuts_bot with (1 := pr1 (pr2 y')).
        pattern (pr1 y') at 2;
          rewrite <- (minusNonnegativeRationals_plus_r y (pr1 y')).
        rewrite iscomm_plusNonnegativeRationals.
        apply plusNonnegativeRationals_lecompat_l.
        now apply lt_leNonnegativeRationals, H.
        apply lt_leNonnegativeRationals ; apply_pr2 ispositive_minusNonnegativeRationals.
        exact Hy.
  - intros Hxy ; unfold neg.
    apply (hinhuniv (P := make_hProp _ isapropempty)) ;
    intros r.
    refine (pr1 (pr2 r) _).
    refine (Hxy _ _).
    exact (pr2 (pr2 r)).
Qed.

Lemma istrans_Dcuts_lt_le_rel :
   x y z : Dcuts_set, Dcuts_lt_rel x y Dcuts_le_rel y z Dcuts_lt_rel x z.
Proof.
  intros x y z Hlt Hle.
  revert Hlt ; apply hinhfun ; intros r.
   (pr1 r) ; split.
  - exact (pr1 (pr2 r)).
  - refine (Hle _ _).
    exact (pr2 (pr2 r)).
Qed.
Lemma istrans_Dcuts_le_lt_rel :
   x y z : Dcuts_set, Dcuts_le_rel x y Dcuts_lt_rel y z Dcuts_lt_rel x z.
Proof.
  intros x y z Hle.
  apply hinhfun ; intros r.
   (pr1 r) ; split.
  - intros Xr ; apply (pr1 (pr2 r)).
    now refine (Hle _ _).
  - exact (pr2 (pr2 r)).
Qed.

Lemma iseo_Dcuts_le_lt_rel :
  isEffectiveOrder Dcuts_le_rel Dcuts_lt_rel.
Proof.
  split.
  - split.
    + exact ispreorder_Dcuts_le_rel.
    + exact isstpo_Dcuts_lt_rel.
  - repeat split.
    + now apply Dcuts_le_ngt_rel.
    + apply (pr2 (Dcuts_le_ngt_rel _ _)).
    + exact istrans_Dcuts_lt_le_rel.
    + exact istrans_Dcuts_le_lt_rel.
Qed.

Definition iseo_Dcuts : EffectiveOrder Dcuts_set :=
  pairEffectiveOrder Dcuts_le_rel Dcuts_lt_rel iseo_Dcuts_le_lt_rel.

Definition eo_Dcuts : EffectivelyOrderedSet :=
  pairEffectivelyOrderedSet iseo_Dcuts.

Definition Dcuts_le : po Dcuts_set := @EOle eo_Dcuts.
Definition Dcuts_ge : po Dcuts_set := @EOge eo_Dcuts.
Definition Dcuts_lt : StrongOrder Dcuts_set := @EOlt eo_Dcuts.
Definition Dcuts_gt : StrongOrder Dcuts_set := @EOgt eo_Dcuts.

Notation "x <= y" := (@EOle_rel eo_Dcuts x y) : Dcuts_scope.
Notation "x >= y" := (@EOge_rel eo_Dcuts x y) : Dcuts_scope.
Notation "x < y" := (@EOlt_rel eo_Dcuts x y) : Dcuts_scope.
Notation "x > y" := (@EOgt_rel eo_Dcuts x y) : Dcuts_scope.

Equivalence on Dcuts


Definition Dcuts_eq_rel :=
  λ X Y : Dcuts_set, r : NonnegativeRationals, (r X r Y) × (r Y r X).
Lemma isaprop_Dcuts_eq_rel : X Y : Dcuts_set, isaprop (Dcuts_eq_rel X Y).
Proof.
  intros X Y.
  apply impred_isaprop ; intro r.
  apply isapropdirprod.
  - now apply isapropimpl, pr2.
  - now apply isapropimpl, pr2.
Qed.
Definition Dcuts_eq : hrel Dcuts_set :=
  λ X Y : Dcuts_set, make_hProp ( r, (r X r Y) × (r Y r X)) (isaprop_Dcuts_eq_rel X Y).

Lemma istrans_Dcuts_eq : istrans Dcuts_eq.
Proof.
  intros x y z Hxy Hyz r.
  split.
  - intros Xr.
    now apply (pr1 (Hyz r)), (pr1 (Hxy r)), Xr.
  - intros Zr.
    now apply (pr2 (Hxy r)), (pr2 (Hyz r)), Zr.
Qed.
Lemma isrefl_Dcuts_eq : isrefl Dcuts_eq.
Proof.
  intros x r.
  now split.
Qed.
Lemma ispreorder_Dcuts_eq : ispreorder Dcuts_eq.
Proof.
  split.
  exact istrans_Dcuts_eq.
  exact isrefl_Dcuts_eq.
Qed.

Lemma issymm_Dcuts_eq : issymm Dcuts_eq.
Proof.
  intros x y Hxy r.
  split.
  exact (pr2 (Hxy r)).
  exact (pr1 (Hxy r)).
Qed.

Lemma iseqrel_Dcuts_eq : iseqrel Dcuts_eq.
Proof.
  split.
  exact ispreorder_Dcuts_eq.
  exact issymm_Dcuts_eq.
Qed.

Lemma Dcuts_eq_is_eq :
   x y : Dcuts_set,
    Dcuts_eq x y x = y.
Proof.
  intros x y Heq.
  apply subtypePath_prop.
  apply funextsec.
  intro r.
  apply hPropUnivalence.
  exact (pr1 (Heq r)).
  exact (pr2 (Heq r)).
Qed.

Apartness on Dcuts


Lemma isaprop_Dcuts_ap_rel (X Y : Dcuts_set) :
  isaprop ((X < Y) ⨿ (Y < X)).
Proof.
  apply (isapropcoprod (X < Y) (Y < X)
                       (propproperty (X < Y))
                       (propproperty (Y < X))
                       (λ Hlt : X < Y, pr2 (Dcuts_le_ngt_rel Y X) (Dcuts_lt_le_rel X Y Hlt))).
Qed.
Definition Dcuts_ap_rel (X Y : Dcuts_set) : hProp :=
  make_hProp ((X < Y) ⨿ (Y < X)) (isaprop_Dcuts_ap_rel X Y).

Lemma isirrefl_Dcuts_ap_rel : isirrefl Dcuts_ap_rel.
Proof.
  intros x.
  unfold neg.
  apply sumofmaps.
  now apply isirrefl_Dcuts_lt_rel.
  now apply isirrefl_Dcuts_lt_rel.
Qed.
Lemma issymm_Dcuts_ap_rel : issymm Dcuts_ap_rel.
Proof.
  intros x y.
  apply coprodcomm.
Qed.
Lemma iscotrans_Dcuts_ap_rel : iscotrans Dcuts_ap_rel.
Proof.
  intros x y z.
  apply sumofmaps ; intros Hap.
  - generalize (iscotrans_Dcuts_lt_rel _ y _ Hap) ; apply hinhfun.
    apply sumofmaps ; intros Hy.
    + now left ; left.
    + now right ; left.
  - generalize (iscotrans_Dcuts_lt_rel _ y _ Hap) ; apply hinhfun.
    apply sumofmaps ; intros Hy.
    + now right ; right.
    + now left ; right.
Qed.

Lemma istight_Dcuts_ap_rel : istight Dcuts_ap_rel.
Proof.
  intros X Y Hap.
  apply Dcuts_eq_is_eq.
  intros r ; split ; revert r.
  - change (X Y).
    apply Dcuts_le_ngt_rel.
    intro Hlt ; apply Hap.
    now right.
  - change (Y X).
    apply Dcuts_le_ngt_rel.
    intro Hlt ; apply Hap.
    now left.
Qed.

Definition Dcuts : tightapSet :=
  Dcuts_set ,, Dcuts_ap_rel ,,
    (isirrefl_Dcuts_ap_rel ,, issymm_Dcuts_ap_rel ,, iscotrans_Dcuts_ap_rel) ,,
    istight_Dcuts_ap_rel.

Lemma not_Dcuts_ap_eq :
   x y : Dcuts, ¬ (x y) (x = y).
Proof.
  intros x y.
  now apply istight_Dcuts_ap_rel.
Qed.

Various theorems about order


Lemma Dcuts_ge_le :
   x y : Dcuts, x y y x.
Proof.
  intros.
  assumption.
Qed.
Lemma Dcuts_le_ge :
   x y : Dcuts, x y y x.
Proof.
  intros.
  assumption.
Qed.
Lemma Dcuts_eq_le :
   x y : Dcuts, Dcuts_eq x y x y.
Proof.
  intros x y Heq.
  intro r ;
    now apply (pr1 (Heq _)).
Qed.
Lemma Dcuts_eq_ge :
   x y : Dcuts, Dcuts_eq x y x y.
Proof.
  intros x y Heq.
  apply Dcuts_eq_le.
  now apply issymm_Dcuts_eq.
Qed.
Lemma Dcuts_le_ge_eq :
   x y : Dcuts, x y x y x = y.
Proof.
  intros x y le_xy ge_xy.
  apply Dcuts_eq_is_eq.
  split.
  now refine (le_xy _).
  now refine (ge_xy _).
Qed.

Lemma Dcuts_gt_lt :
   x y : Dcuts, (x > y) (y < x).
Proof.
  now split.
Qed.
Lemma Dcuts_gt_ge :
   x y : Dcuts, x > y x y.
Proof.
  intros x y.
  now apply Dcuts_lt_le_rel.
Qed.

Lemma Dcuts_gt_nle :
   x y : Dcuts, x > y neg (x y).
Proof.
  intros x y Hlt Hle.
  now apply (pr2 (Dcuts_le_ngt_rel _ _)) in Hle.
Qed.
Lemma Dcuts_nlt_ge :
   x y : Dcuts, neg (x < y) (x y).
Proof.
  intros X Y.
  now apply Dcuts_le_ngt_rel.
Qed.
Lemma Dcuts_lt_nge :
   x y : Dcuts, x < y neg (x y).
Proof.
  intros x y.
  now apply Dcuts_gt_nle.
Qed.

Algebraic structures on Dcuts

From non negative rational numbers to Dedekind cuts


Lemma NonnegativeRationals_to_Dcuts_bot (q : NonnegativeRationals) :
  Dcuts_def_bot (λ r : NonnegativeRationals, (r < q)%NRat).
Proof.
  intros r Hr n Hnr.
  now apply istrans_le_lt_ltNonnegativeRationals with r.
Qed.
Lemma NonnegativeRationals_to_Dcuts_open (q : NonnegativeRationals) :
  Dcuts_def_open (λ r : NonnegativeRationals, (r < q)%NRat).
Proof.
  intros r Hr.
  apply hinhpr.
  generalize (between_ltNonnegativeRationals r q Hr) ; intros n.
   (pr1 n).
  split.
  exact (pr2 (pr2 n)).
  exact (pr1 (pr2 n)).
Qed.
Lemma NonnegativeRationals_to_Dcuts_corr (q : NonnegativeRationals) :
  Dcuts_def_corr (λ r : NonnegativeRationals, (r < q)%NRat).
Proof.
  intros r Hr0.
  apply hinhpr.
  generalize (isdecrel_ltNonnegativeRationals r q) ; apply sumofmaps ; intros Hqr.
  - right.
    assert (Hn0 : (0 < q - r)%NRat) by (now apply ispositive_minusNonnegativeRationals).
     (q - r).
    split.
    + apply_pr2 (plusNonnegativeRationals_ltcompat_r r).
      rewrite minusNonnegativeRationals_plus_r.
      pattern q at 1 ;
        rewrite <- isrunit_zeroNonnegativeRationals.
      apply plusNonnegativeRationals_ltcompat_l.
      exact Hr0.
      now apply lt_leNonnegativeRationals, Hqr.
    + rewrite minusNonnegativeRationals_plus_r.
      now apply isirrefl_ltNonnegativeRationals.
      now apply lt_leNonnegativeRationals, Hqr.
  - now left.
Qed.

Definition NonnegativeRationals_to_Dcuts (q : NonnegativeRationals) : Dcuts :=
  make_Dcuts (λ r, (r < q)%NRat)
           (NonnegativeRationals_to_Dcuts_bot q)
           (NonnegativeRationals_to_Dcuts_open q)
           (NonnegativeRationals_to_Dcuts_corr q).

Lemma isapfun_NonnegativeRationals_to_Dcuts_aux :
   q q' : NonnegativeRationals,
    NonnegativeRationals_to_Dcuts q < NonnegativeRationals_to_Dcuts q'
     (q < q')%NRat.
Proof.
  intros q q'.
  split.
  - apply hinhuniv.
    intros r.
    apply istrans_le_lt_ltNonnegativeRationals with (pr1 r).
    + apply notlt_geNonnegativeRationals.
      exact (pr1 (pr2 r)).
    + exact (pr2 (pr2 r)).
  - intros H.
    apply hinhpr.
     q ; split.
    now apply (isirrefl_ltNonnegativeRationals q).
    exact H.
Qed.
Lemma isapfun_NonnegativeRationals_to_Dcuts :
   q q' : NonnegativeRationals,
    NonnegativeRationals_to_Dcuts q NonnegativeRationals_to_Dcuts q'
     q != q'.
Proof.
  intros q q'.
  apply sumofmaps ; intros Hap.
  now apply ltNonnegativeRationals_noteq, isapfun_NonnegativeRationals_to_Dcuts_aux.
  now apply gtNonnegativeRationals_noteq, isapfun_NonnegativeRationals_to_Dcuts_aux.
Qed.
Lemma isapfun_NonnegativeRationals_to_Dcuts' :
   q q' : NonnegativeRationals,
    q != q'
     NonnegativeRationals_to_Dcuts q NonnegativeRationals_to_Dcuts q'.
Proof.
  intros q q' H.
  apply noteq_ltorgtNonnegativeRationals in H.
  induction H as [H | H].
  now left ; apply (pr2 (isapfun_NonnegativeRationals_to_Dcuts_aux _ _)).
  now right ; apply (pr2 (isapfun_NonnegativeRationals_to_Dcuts_aux _ _)).
Qed.

Definition Dcuts_zero : Dcuts := NonnegativeRationals_to_Dcuts 0%NRat.
Definition Dcuts_one : Dcuts := NonnegativeRationals_to_Dcuts 1%NRat.
Definition Dcuts_two : Dcuts := NonnegativeRationals_to_Dcuts 2.

Notation "0" := Dcuts_zero : Dcuts_scope.
Notation "1" := Dcuts_one : Dcuts_scope.
Notation "2" := Dcuts_two : Dcuts_scope.

Various usefull theorems

Lemma Dcuts_zero_empty :
   r : NonnegativeRationals, neg (r 0).
Proof.
  intros r ; simpl.
  change (neg (r < 0)%NRat).
  now apply isnonnegative_NonnegativeRationals'.
Qed.
Lemma Dcuts_notempty_notzero :
   (x : Dcuts) (r : NonnegativeRationals), r x x 0.
Proof.
  intros x r Hx.
  right.
  apply hinhpr.
   r.
  split.
  now apply Dcuts_zero_empty.
  exact Hx.
Qed.

Lemma Dcuts_ge_0 :
   x : Dcuts, Dcuts_zero x.
Proof.
  intros x r Hr.
  apply fromempty.
  revert Hr.
  now apply Dcuts_zero_empty.
Qed.
Lemma Dcuts_notlt_0 :
   x : Dcuts, ¬ (x < Dcuts_zero).
Proof.
  intros x.
  unfold neg.
  apply hinhuniv'.
  exact isapropempty.
  intros r.
  exact (Dcuts_zero_empty _ (pr2 (pr2 r))).
Qed.

Lemma Dcuts_apzero_notempty :
   (x : Dcuts), (0%NRat x) x 0.
Proof.
  intros x ; split.
  - now apply Dcuts_notempty_notzero.
  - apply sumofmaps.
    + apply hinhuniv ; intros r.
      apply fromempty.
      now apply (Dcuts_zero_empty _ (pr2 (pr2 r))).
    + apply hinhuniv ; intros r.
      apply is_Dcuts_bot with (1 := pr2 (pr2 r)).
      now apply isnonnegative_NonnegativeRationals.
Qed.

Lemma NonnegativeRationals_to_Dcuts_notin_le :
   (x : Dcuts) (r : NonnegativeRationals),
    ¬ (r x) x NonnegativeRationals_to_Dcuts r.
Proof.
  intros x r Hr q Hq.
  simpl.
  now apply (Dcuts_finite x).
Qed.

Addition in Dcuts


Section Dcuts_plus.

  Context (X : hsubtype NonnegativeRationals).
  Context (X_bot : Dcuts_def_bot X).
  Context (X_open : Dcuts_def_open X).
  Context (X_corr : Dcuts_def_corr X).
  Context (Y : hsubtype NonnegativeRationals).
  Context (Y_bot : Dcuts_def_bot Y).
  Context (Y_open : Dcuts_def_open Y).
  Context (Y_corr : Dcuts_def_corr Y).

Definition Dcuts_plus_val : hsubtype NonnegativeRationals :=
  λ r : NonnegativeRationals,
        ((X r) ⨿ (Y r))
        ( xy : NonnegativeRationals × NonnegativeRationals, (r = (pr1 xy + pr2 xy)%NRat) × ((X (pr1 xy)) × (Y (pr2 xy)))).

Lemma Dcuts_plus_bot : Dcuts_def_bot Dcuts_plus_val.
Proof.
  intros r Hr n Hn.
  revert Hr ; apply hinhfun ;
  apply sumofmaps ; [apply sumofmaps ; intros Hr | intros xy].
  - left ; left.
    now apply X_bot with r.
  - left ; right.
    now apply Y_bot with r.
  - right.
    generalize (isdeceq_NonnegativeRationals r 0%NRat) ; apply sumofmaps ; intros Hr0.
    + rewrite Hr0 in Hn.
      apply NonnegativeRationals_eq0_le0 in Hn.
       (0%NRat,,0%NRat).
      rewrite Hn ; simpl.
      repeat split.
      × now rewrite isrunit_zeroNonnegativeRationals.
      × apply X_bot with (1 := pr1 (pr2 (pr2 xy))).
        apply isnonnegative_NonnegativeRationals.
      × apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
        apply isnonnegative_NonnegativeRationals.
    + set (nx := (pr1 (pr1 xy) × (n / r))%NRat).
      set (ny := (pr2 (pr1 xy) × (n / r))%NRat).
       (nx,,ny).
      repeat split.
      × unfold nx,ny ; simpl.
        rewrite <- isrdistr_mult_plusNonnegativeRationals, <- (pr1 (pr2 xy)).
        rewrite multdivNonnegativeRationals.
        reflexivity.
        now apply NonnegativeRationals_neq0_gt0.
      × apply X_bot with (1 := pr1 (pr2 (pr2 xy))).
        apply multNonnegativeRationals_le1_r.
        now apply divNonnegativeRationals_le1.
      × apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
        apply multNonnegativeRationals_le1_r.
        now apply divNonnegativeRationals_le1.
Qed.

Lemma Dcuts_plus_open : Dcuts_def_open Dcuts_plus_val.
Proof.
  intros r.
  apply hinhuniv, sumofmaps.
  - apply sumofmaps ; intro Hr.
    + generalize (X_open r Hr).
      apply hinhfun ; intros n.
       (pr1 n).
      split.
      × apply hinhpr ; left ; left.
        exact (pr1 (pr2 n)).
      × exact (pr2 (pr2 n)).
    + generalize (Y_open r Hr).
      apply hinhfun ; intros n.
       (pr1 n).
      split.
      × apply hinhpr ; left ; right.
        exact (pr1 (pr2 n)).
      × exact (pr2 (pr2 n)).
  - intros xy.
    generalize (X_open _ (pr1 (pr2 (pr2 xy)))) (Y_open _ (pr2 (pr2 (pr2 xy)))).
    apply hinhfun2.
    intros nx ny.
     (pr1 nx + pr1 ny).
    split.
    + apply hinhpr ; right ; (pr1 nx ,, pr1 ny).
      repeat split.
      × exact (pr1 (pr2 nx)).
      × exact (pr1 (pr2 ny)).
    + pattern r at 1 ;
      rewrite (pr1 (pr2 xy)).
      apply plusNonnegativeRationals_ltcompat.
      exact (pr2 (pr2 nx)).
      exact (pr2 (pr2 ny)).
Qed.
Lemma Dcuts_plus_corr : Dcuts_def_corr Dcuts_plus_val.
Proof.
  intros c Hc.
  apply ispositive_NQhalf in Hc.
  generalize (X_corr _ Hc) (Y_corr _ Hc).
  apply hinhfun2 ; apply (sumofmaps (Z := _ _)) ; intros Hx ; apply sumofmaps ; intros Hy.
  - left.
    unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps.
    + apply sumofmaps ; intros Hz.
      × apply Hx.
        apply X_bot with (1 := Hz).
        pattern c at 2 ; rewrite (NQhalf_double c).
        apply plusNonnegativeRationals_le_r.
      × apply Hy.
        apply Y_bot with (1 := Hz).
        pattern c at 2 ; rewrite (NQhalf_double c).
        apply plusNonnegativeRationals_le_r.
    + intros xy.
      generalize (isdecrel_ltNonnegativeRationals (pr1 (pr1 xy)) (c / 2)%NRat) ;
        apply sumofmaps ; intros Hx'.
      generalize (isdecrel_ltNonnegativeRationals (pr2 (pr1 xy)) (c / 2)%NRat) ;
        apply sumofmaps ; intros Hy'.
      × apply (isirrefl_StrongOrder ltNonnegativeRationals c).
        pattern c at 2 ; rewrite (NQhalf_double c).
        pattern c at 1 ; rewrite (pr1 (pr2 xy)).
        apply plusNonnegativeRationals_ltcompat.
        exact Hx'.
        exact Hy'.
      × apply Hy.
        apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
        now apply notlt_geNonnegativeRationals ; apply Hy'.
      × apply Hx.
        apply X_bot with (1 := pr1 (pr2 (pr2 xy))).
        now apply notlt_geNonnegativeRationals ; apply Hx'.
  - right.
    rename Hy into q.
     (pr1 q) ; split.
    apply hinhpr.
    left ; right ; exact (pr1 (pr2 q)).
    unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps.
    apply sumofmaps ; [intros Xq | intros Yq'].
    + apply Hx ; apply X_bot with (1 := Xq).
      pattern c at 2;
        rewrite (NQhalf_double c).
      rewrite <- isassoc_plusNonnegativeRationals.
      apply plusNonnegativeRationals_le_l.
    + apply (pr2 (pr2 q)) ; apply Y_bot with (1 := Yq').
      pattern c at 2;
        rewrite (NQhalf_double c).
      rewrite <- isassoc_plusNonnegativeRationals.
      apply plusNonnegativeRationals_le_r.
    + intros xy.
      apply (isirrefl_StrongOrder ltNonnegativeRationals (pr1 q + c)).
      pattern c at 2;
        rewrite (NQhalf_double c).
      pattern (pr1 q + c) at 1 ; rewrite (pr1 (pr2 xy)).
      rewrite <- isassoc_plusNonnegativeRationals.
      rewrite iscomm_plusNonnegativeRationals.
      apply plusNonnegativeRationals_ltcompat.
      apply notge_ltNonnegativeRationals ; intro H.
      apply (pr2 (pr2 q)) ; apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
      exact H.
      apply notge_ltNonnegativeRationals ; intro H.
      apply Hx ; apply X_bot with (1 := pr1 (pr2 (pr2 xy))).
      exact H.
  - right.
    rename Hx into q.
     (pr1 q) ; split.
    apply hinhpr.
    left ; left ; exact (pr1 (pr2 q)).
    unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps.
    apply sumofmaps ; [intros Xq' | intros Yq].
    + apply (pr2 (pr2 q)) ; apply X_bot with (1 := Xq').
      pattern c at 2;
        rewrite (NQhalf_double c).
      rewrite <- isassoc_plusNonnegativeRationals.
      apply plusNonnegativeRationals_le_r.
    + apply Hy ; apply Y_bot with (1 := Yq).
      pattern c at 2;
        rewrite (NQhalf_double c).
      rewrite <- isassoc_plusNonnegativeRationals.
      apply plusNonnegativeRationals_le_l.
    + intros xy.
      apply (isirrefl_StrongOrder ltNonnegativeRationals (pr1 q + c)).
      pattern c at 2; rewrite (NQhalf_double c).
      pattern (pr1 q + c) at 1 ; rewrite (pr1 (pr2 xy)).
      rewrite <- isassoc_plusNonnegativeRationals.
      apply plusNonnegativeRationals_ltcompat.
      apply notge_ltNonnegativeRationals ; intro H.
      apply (pr2 (pr2 q)) ; apply X_bot with (1 := pr1 (pr2 (pr2 xy))).
      exact H.
      apply notge_ltNonnegativeRationals ; intro H.
      apply Hy ; apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
      exact H.
  - right.
    rename Hx into qx ; rename Hy into qy.
     (pr1 qx + pr1 qy).
    split.
    + apply hinhpr.
      right.
       (pr1 qx,,pr1 qy) ; repeat split.
      × exact (pr1 (pr2 qx)).
      × exact (pr1 (pr2 qy)).
    + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps.
      apply sumofmaps ; [ intros Xq' | intros Yq'].
      × apply (pr2 (pr2 qx)), X_bot with (1 := Xq').
        pattern c at 2;
          rewrite (NQhalf_double c).
        rewrite <- isassoc_plusNonnegativeRationals.
        apply plusNonnegativeRationals_lecompat_r.
        rewrite isassoc_plusNonnegativeRationals.
        apply plusNonnegativeRationals_le_r.
      × apply (pr2 (pr2 qy)), Y_bot with (1 := Yq').
        pattern c at 2;
          rewrite (NQhalf_double c).
        rewrite <- isassoc_plusNonnegativeRationals.
        apply plusNonnegativeRationals_lecompat_r.
        eapply istrans_leNonnegativeRationals, plusNonnegativeRationals_le_r.
        apply plusNonnegativeRationals_le_l.
      × intros xy.
        apply (isirrefl_StrongOrder ltNonnegativeRationals (pr1 qx + pr1 qy + c)).
        pattern c at 2; rewrite (NQhalf_double c).
        pattern (pr1 qx + pr1 qy + c) at 1 ; rewrite (pr1 (pr2 xy)).
        rewrite <- isassoc_plusNonnegativeRationals.
        rewrite (isassoc_plusNonnegativeRationals (pr1 qx) (pr1 qy) (c / 2)%NRat).
        rewrite (iscomm_plusNonnegativeRationals (pr1 qy)).
        rewrite <- isassoc_plusNonnegativeRationals.
        rewrite (isassoc_plusNonnegativeRationals (pr1 qx + (c/2)%NRat)).
        apply plusNonnegativeRationals_ltcompat.
        apply notge_ltNonnegativeRationals ; intro H.
        apply (pr2 (pr2 qx)) ; apply X_bot with (1 := pr1 (pr2 (pr2 xy))) ; exact H.
        apply notge_ltNonnegativeRationals ; intro H.
        apply (pr2 (pr2 qy)) ; apply Y_bot with (1 := pr2 (pr2 (pr2 xy))) ; exact H.
Qed.

End Dcuts_plus.

Definition Dcuts_plus (X Y : Dcuts) : Dcuts :=
  make_Dcuts (Dcuts_plus_val (pr1 X) (pr1 Y))
           (Dcuts_plus_bot (pr1 X) (is_Dcuts_bot X)
                           (pr1 Y) (is_Dcuts_bot Y))
           (Dcuts_plus_open (pr1 X) (is_Dcuts_open X)
                            (pr1 Y) (is_Dcuts_open Y))
           (Dcuts_plus_corr (pr1 X) (is_Dcuts_bot X) (is_Dcuts_corr X)
                             (pr1 Y) (is_Dcuts_bot Y) (is_Dcuts_corr Y)).

Multiplication in Dcuts


Section Dcuts_NQmult.

  Context (x : NonnegativeRationals).
  Context (Hx : (0 < x)%NRat).
  Context (Y : hsubtype NonnegativeRationals).
  Context (Y_bot : Dcuts_def_bot Y).
  Context (Y_open : Dcuts_def_open Y).
  Context (Y_finite : Dcuts_def_finite Y).
  Context (Y_corr : Dcuts_def_corr Y).

Definition Dcuts_NQmult_val : hsubtype NonnegativeRationals :=
  λ r, ry : NonnegativeRationals, r = x × ry × Y ry.

Lemma Dcuts_NQmult_bot : Dcuts_def_bot Dcuts_NQmult_val.
Proof.
  intros r Hr n Hn.
  revert Hr ; apply hinhfun ;
  intros ry.
  generalize (isdeceq_NonnegativeRationals r 0%NRat) ;
    apply sumofmaps ; intros Hr0.
  - rewrite Hr0 in Hn.
    apply NonnegativeRationals_eq0_le0 in Hn.
     0%NRat.
    rewrite Hn ; simpl.
    split.
    + now rewrite israbsorb_zero_multNonnegativeRationals.
    + apply Y_bot with (1 := pr2 (pr2 ry)).
      apply isnonnegative_NonnegativeRationals.
  - set (ny := pr1 ry × (n / r)%NRat).
     ny.
    split.
    + unfold ny ; simpl.
      rewrite <- isassoc_multNonnegativeRationals, <- (pr1 (pr2 ry)).
      rewrite multdivNonnegativeRationals.
      reflexivity.
      now apply NonnegativeRationals_neq0_gt0.
    + apply Y_bot with (1 := pr2 (pr2 ry)).
      apply multNonnegativeRationals_le1_r.
      now apply divNonnegativeRationals_le1.
Qed.
Lemma Dcuts_NQmult_open : Dcuts_def_open Dcuts_NQmult_val.
Proof.
  intros r.
  apply hinhuniv ; intros ry.
  generalize (Y_open _ (pr2 (pr2 ry))).
  apply hinhfun.
  intros ny.

   (x × pr1 ny).
  split.
  - apply hinhpr ; (pr1 ny).
    split.
    + reflexivity.
    + exact (pr1 (pr2 ny)).
  - pattern r at 1 ; rewrite (pr1 (pr2 ry)).
    apply multNonnegativeRationals_ltcompat_l.
    exact Hx.
    exact (pr2 (pr2 ny)).
Qed.
Lemma Dcuts_NQmult_finite : Dcuts_def_finite Dcuts_NQmult_val.
Proof.
  revert Y_finite.
  apply hinhfun.
  intros y.
   (x × pr1 y).
  unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ;
  intros ry.
  generalize (pr1 (pr2 ry)).
  apply gtNonnegativeRationals_noteq.
  apply (pr2 (lt_gtNonnegativeRationals _ _)).
  apply (multNonnegativeRationals_ltcompat_l x (pr1 ry) (pr1 y) Hx).
  apply notge_ltNonnegativeRationals.
  intro Hy' ; apply (pr2 y).
  apply Y_bot with (pr1 ry).
  exact (pr2 (pr2 ry)).
  exact Hy'.
Qed.

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.
     (x × pr1 q).
    split.
    + apply hinhpr.
       (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.

End Dcuts_NQmult.

Definition Dcuts_NQmult x (Y : Dcuts) Hx : Dcuts :=
  make_Dcuts (Dcuts_NQmult_val x (pr1 Y))
           (Dcuts_NQmult_bot x (pr1 Y) (is_Dcuts_bot Y))
           (Dcuts_NQmult_open x Hx (pr1 Y) (is_Dcuts_open Y))
           (Dcuts_NQmult_corr x Hx (pr1 Y) (is_Dcuts_bot Y) (is_Dcuts_corr Y)).

Section Dcuts_mult.

  Context (X : hsubtype NonnegativeRationals).
  Context (X_bot : Dcuts_def_bot X).
  Context (X_open : Dcuts_def_open X).
  Context (X_finite : Dcuts_def_finite X).
  Context (X_corr : Dcuts_def_corr X).
  Context (Y : hsubtype NonnegativeRationals).
  Context (Y_bot : Dcuts_def_bot Y).
  Context (Y_open : Dcuts_def_open Y).
  Context (Y_finite : Dcuts_def_finite Y).
  Context (Y_corr : Dcuts_def_corr Y).

Definition Dcuts_mult_val : hsubtype NonnegativeRationals :=
  λ r, xy : NonnegativeRationals × NonnegativeRationals,
                           r = (pr1 xy × pr2 xy)%NRat × X (pr1 xy) × Y (pr2 xy).

Lemma Dcuts_mult_bot : Dcuts_def_bot Dcuts_mult_val.
Proof.
  intros r Hr n Hn.
  revert Hr ; apply hinhfun ;
  intros xy.
  generalize (isdeceq_NonnegativeRationals r 0%NRat) ;
    apply sumofmaps ; intros Hr0.
  - rewrite Hr0 in Hn.
    apply NonnegativeRationals_eq0_le0 in Hn.
     (0%NRat,,0%NRat).
    rewrite Hn ; simpl.
    repeat split.
    + now rewrite israbsorb_zero_multNonnegativeRationals.
    + apply X_bot with (1 := pr1 (pr2 (pr2 xy))).
      apply isnonnegative_NonnegativeRationals.
    + apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
      apply isnonnegative_NonnegativeRationals.
  - set (nx := pr1 (pr1 xy)).
    set (ny := (pr2 (pr1 xy) × (n / r))%NRat).
     (nx,,ny).
    repeat split.
    + unfold nx,ny ; simpl.
      rewrite <- isassoc_multNonnegativeRationals, <- (pr1 (pr2 xy)).
      rewrite multdivNonnegativeRationals.
      reflexivity.
      now apply NonnegativeRationals_neq0_gt0.
    + exact (pr1 (pr2 (pr2 xy))).
    + apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
      apply multNonnegativeRationals_le1_r.
      now apply divNonnegativeRationals_le1.
Qed.
Lemma Dcuts_mult_open : Dcuts_def_open Dcuts_mult_val.
Proof.
  intros r.
  apply hinhuniv ; intros xy.
  generalize (X_open _ (pr1 (pr2 (pr2 xy)))) (Y_open _ (pr2 (pr2 (pr2 xy)))).
  apply hinhfun2.
  intros nx ny.
   (pr1 nx × pr1 ny).
  split.
  - apply hinhpr ; (pr1 nx ,, pr1 ny).
    repeat split.
    + exact (pr1 (pr2 nx)).
    + exact (pr1 (pr2 ny)).
  - pattern r at 1 ; rewrite (pr1 (pr2 xy)).
    apply multNonnegativeRationals_ltcompat.
    exact (pr2 (pr2 nx)).
    exact (pr2 (pr2 ny)).
Qed.
Lemma Dcuts_mult_finite : Dcuts_def_finite Dcuts_mult_val.
Proof.
  revert X_finite Y_finite.
  apply hinhfun2.
  intros x y.
   (pr1 x × pr1 y).
  unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ;
  intros xy.
  generalize (isdecrel_ltNonnegativeRationals (pr1 (pr1 xy)) (pr1 x)) ; apply sumofmaps ; intros Hx'.
  generalize (isdecrel_ltNonnegativeRationals (pr2 (pr1 xy)) (pr1 y)) ; apply sumofmaps ; intros Hy'.
  - apply (isirrefl_StrongOrder ltNonnegativeRationals (pr1 x × pr1 y)).
    pattern (pr1 x × pr1 y) at 1 ; rewrite (pr1 (pr2 xy)).
    now apply multNonnegativeRationals_ltcompat.
  - apply (pr2 y).
    apply Y_bot with (1 := pr2 (pr2 (pr2 xy))).
    now apply notlt_geNonnegativeRationals ; apply Hy'.
  - apply (pr2 x).
    apply X_bot with (1 := pr1 (pr2 (pr2 xy))).
    now apply notlt_geNonnegativeRationals ; apply Hx'.
Qed.

Context (Hx1 : ¬ X 1%NRat).

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.
       (pr1 x × pr1 y) ; repeat split.
      × apply hinhpr.
         (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.

End Dcuts_mult.

Section Dcuts_mult'.

  Context (X : hsubtype NonnegativeRationals).
  Context (X_bot : Dcuts_def_bot X).
  Context (X_open : Dcuts_def_open X).
  Context (X_finite : Dcuts_def_finite X).
  Context (X_corr : Dcuts_def_corr X).
  Context (Y : hsubtype NonnegativeRationals).
  Context (Y_bot : Dcuts_def_bot Y).
  Context (Y_open : Dcuts_def_open Y).
  Context (Y_finite : Dcuts_def_finite Y).
  Context (Y_corr : Dcuts_def_corr Y).

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.
         (r / (pr1 x + 1))%NRat ; split.
        + now rewrite multdivNonnegativeRationals.
        + apply hinhpr.
           (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.
             (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')).
         (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.

End Dcuts_mult'.

Definition Dcuts_mult (X Y : Dcuts) : Dcuts :=
  make_Dcuts (Dcuts_mult_val (pr1 X) (pr1 Y))
           (Dcuts_mult_bot (pr1 X) (is_Dcuts_bot X)
                           (pr1 Y) (is_Dcuts_bot Y))
           (Dcuts_mult_open (pr1 X) (is_Dcuts_open X)
                            (pr1 Y) (is_Dcuts_open Y))
           (Dcuts_mult_corr (pr1 X) (is_Dcuts_bot X) (is_Dcuts_corr X)
                             (pr1 Y) (is_Dcuts_bot Y) (is_Dcuts_corr Y)).

Multiplicative inverse in Dcuts


Section Dcuts_inv.

Context (X : hsubtype NonnegativeRationals).
Context (X_bot : Dcuts_def_bot X).
Context (X_open : Dcuts_def_open X).
Context (X_finite : Dcuts_def_finite X).
Context (X_corr : Dcuts_def_corr X).
Context (X_0 : X 0%NRat).

Definition Dcuts_inv_val : hsubtype NonnegativeRationals :=
  λ r : NonnegativeRationals,
        hexists (λ l : NonnegativeRationals, ( rx : NonnegativeRationals, X rx (r × rx l)%NRat)
                                               × (0 < l)%NRat × (l < 1)%NRat).

Lemma Dcuts_inv_in :
   x, (0 < x)%NRat X x (Dcuts_inv_val (/ x)%NRat) empty.
Proof.
  intros x Hx0 Xx.
  unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros l.
  set (H := pr1 (pr2 l) _ Xx).
  rewrite islinv_NonnegativeRationals in H.
  apply (pr2 (notlt_geNonnegativeRationals _ _)) in H.
  now apply H, (pr2 (pr2 (pr2 l))).
  exact Hx0.
Qed.
Lemma Dcuts_inv_out :
   x, ¬ (X x) y, (x < y)%NRat Dcuts_inv_val (/ y)%NRat.
Proof.
  intros x nXx y Hy.
  apply hinhpr.
   (x / y)%NRat ; repeat split.
  - intros rx Hrx.
    unfold divNonnegativeRationals.
    rewrite iscomm_multNonnegativeRationals.
    apply multNonnegativeRationals_lecompat_r.
    apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals.
    intros H ; apply nXx.
    now apply X_bot with (1 := Hrx).
  - apply ispositive_divNonnegativeRationals.
    apply notge_ltNonnegativeRationals.
    intros H ; apply nXx.
    now apply X_bot with (1 := X_0).
    apply istrans_le_lt_ltNonnegativeRationals with (2 := Hy).
    now apply isnonnegative_NonnegativeRationals.
  - apply_pr2 (multNonnegativeRationals_ltcompat_r y).
    apply istrans_le_lt_ltNonnegativeRationals with (2 := Hy).
    now apply isnonnegative_NonnegativeRationals.
    unfold divNonnegativeRationals.
    rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, islunit_oneNonnegativeRationals, isrunit_oneNonnegativeRationals.
    exact Hy.
    apply istrans_le_lt_ltNonnegativeRationals with (2 := Hy).
    now apply isnonnegative_NonnegativeRationals.
Qed.

Lemma Dcuts_inv_bot : Dcuts_def_bot Dcuts_inv_val.
Proof.
  intros r Hr q Hq.
  revert Hr.
  apply hinhfun ; intros l.
   (pr1 l) ; repeat split.
  - intros rx Xrx.
    apply istrans_leNonnegativeRationals with (2 := pr1 (pr2 l) _ Xrx).
    now apply multNonnegativeRationals_lecompat_r.
  - exact (pr1 (pr2 (pr2 l))).
  - exact (pr2 (pr2 (pr2 l))).
Qed.

Lemma Dcuts_inv_open : Dcuts_def_open Dcuts_inv_val.
Proof.
  intros r.
  apply hinhuniv.
  intros l.
  generalize (eq0orgt0NonnegativeRationals r) ; apply sumofmaps ; intros Hr0.
  - rewrite Hr0 in l |- × ; clear r Hr0.
    revert X_finite.
    apply hinhfun.
    intros r'.
    set (r := NQmax 2%NRat (pr1 r')).
    assert (Hr1 : (1 < r)%NRat).
    { apply istrans_lt_le_ltNonnegativeRationals with (2 := NQmax_le_l _ _).
      exact one_lt_twoNonnegativeRationals. }
    assert (Hr0 : (0 < r)%NRat).
    { simple refine (istrans_le_lt_ltNonnegativeRationals _ _ _ _ Hr1).
      now apply isnonnegative_NonnegativeRationals. }
     (/ (r × r))%NRat ; split.
    + apply hinhpr.
       (/ r)%NRat ; repeat split.
      × intros rx Xrx.
        apply (multNonnegativeRationals_lecompat_l' (r × r)).
        now apply ispositive_multNonnegativeRationals.
        rewrite <- isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, islunit_oneNonnegativeRationals.
        rewrite isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals.
        apply istrans_leNonnegativeRationals with (2 := NQmax_le_r _ _).
        apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals ; intro H ; apply (pr2 r').
        now apply X_bot with (1 := Xrx).
        exact Hr0.
        now apply ispositive_multNonnegativeRationals.
      × now apply ispositive_invNonnegativeRationals.
      × apply_pr2 (multNonnegativeRationals_ltcompat_l r).
        assumption.
        now rewrite isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals.
    + apply ispositive_invNonnegativeRationals.
      now apply ispositive_multNonnegativeRationals.
  - set (l' := between_ltNonnegativeRationals _ _ (pr2 (pr2 (pr2 l)))).
    apply hinhpr.
     ((pr1 l'/pr1 l) × r)%NRat ; split.
    + apply hinhpr.
       (pr1 l') ; repeat split.
      × intros rx Xrx.
        rewrite isassoc_multNonnegativeRationals.
        pattern l' at 1 ;
          rewrite <- (multdivNonnegativeRationals (pr1 l') (pr1 l)), iscomm_multNonnegativeRationals.
        apply multNonnegativeRationals_lecompat_r.
        now apply (pr1 (pr2 l)).
        exact (pr1 (pr2 (pr2 l))).
      × apply istrans_le_lt_ltNonnegativeRationals with (2 := pr1 (pr2 l')).
        now apply isnonnegative_NonnegativeRationals.
      × exact (pr2 (pr2 l')).
    + pattern r at 1 ; rewrite <- (islunit_oneNonnegativeRationals r).
      apply multNonnegativeRationals_ltcompat_r.
      exact Hr0.
      apply_pr2 (multNonnegativeRationals_ltcompat_r (pr1 l)).
      exact (pr1 (pr2 (pr2 l))).
      rewrite islunit_oneNonnegativeRationals.
      rewrite iscomm_multNonnegativeRationals, multdivNonnegativeRationals.
      exact (pr1 (pr2 l')).
      exact (pr1 (pr2 (pr2 l))).
Qed.

Context (X_1 : X 1%NRat).

Lemma Dcuts_inv_corr_aux : Dcuts_def_corr Dcuts_inv_val.
Proof.
  assert ( c, (0 < c)%NRat hexists (λ q : NonnegativeRationals, X q × ¬ X (q + c))).
  { intros c Hc0.
    generalize (X_corr c Hc0) ; apply hinhuniv ; apply sumofmaps ; [ intros nXc | intros H].
    - apply hinhpr.
       0%NRat ; split.
      + exact X_0.
      + now rewrite islunit_zeroNonnegativeRationals.
    - apply hinhpr ; exact H. }
  clear X_corr ; rename X0 into X_corr.

  intros c Hc0.
  apply ispositive_NQhalf in Hc0.
  specialize (X_corr _ Hc0) ; revert X_corr.
  apply hinhfun ; intros r.
  right.
   (/ (NQmax 1%NRat (pr1 r) + c))%NRat ; split.
  - apply Dcuts_inv_out with (1 := pr2 (pr2 r)).
    pattern c at 2; rewrite (NQhalf_double c), <- isassoc_plusNonnegativeRationals.
    eapply istrans_le_lt_ltNonnegativeRationals, plusNonnegativeRationals_lt_r.
    apply plusNonnegativeRationals_lecompat_r ; apply NQmax_le_r.
    exact Hc0.
  - assert (Xmax : X (NQmax 1%NRat (pr1 r))).
    { apply NQmax_case.
      exact X_1.
      exact (pr1 (pr2 r)). }
    assert (Hmax : (0 < NQmax 1 (pr1 r))%NRat).
    { eapply istrans_lt_le_ltNonnegativeRationals, NQmax_le_l.
      now eapply ispositive_oneNonnegativeRationals. }
    intro Hinv ; apply (Dcuts_inv_in _ Hmax Xmax), Dcuts_inv_bot with (1 := Hinv).
    apply lt_leNonnegativeRationals, minusNonnegativeRationals_ltcompat_l' with (/ (NQmax 1 (pr1 r) + c))%NRat.
    rewrite plusNonnegativeRationals_minus_l.
    rewrite minus_divNonnegativeRationals, plusNonnegativeRationals_minus_l.
    unfold divNonnegativeRationals ;
      apply_pr2 (multNonnegativeRationals_ltcompat_r (NQmax 1 (pr1 r) × (NQmax 1 (pr1 r) + c))%NRat).
    apply ispositive_multNonnegativeRationals.
    exact Hmax.
    now apply ispositive_plusNonnegativeRationals_l.
    rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals.
    apply multNonnegativeRationals_ltcompat_l.
    now apply_pr2 ispositive_NQhalf.
    pattern 1%NRat at 1 ;
      rewrite <- (islunit_oneNonnegativeRationals 1%NRat).
    apply istrans_le_lt_ltNonnegativeRationals with (NQmax 1 (pr1 r) × 1)%NRat.
    now apply multNonnegativeRationals_lecompat_r, NQmax_le_l.
    apply multNonnegativeRationals_ltcompat_l.
    exact Hmax.
    apply istrans_le_lt_ltNonnegativeRationals with (1 := NQmax_le_l _ (pr1 r)).
    apply plusNonnegativeRationals_lt_r.
    now apply_pr2 ispositive_NQhalf.
    apply ispositive_multNonnegativeRationals.
    exact Hmax.
    now apply ispositive_plusNonnegativeRationals_l.
    now apply ispositive_plusNonnegativeRationals_l.
Qed.

End Dcuts_inv.

Section Dcuts_inv'.

Context (X : hsubtype NonnegativeRationals).
Context (X_bot : Dcuts_def_bot X).
Context (X_open : Dcuts_def_open X).
Context (X_finite : Dcuts_def_finite X).
Context (X_corr : Dcuts_def_corr X).
Context (X_0 : X 0%NRat).

Lemma Dcuts_inv_corr : Dcuts_def_corr (Dcuts_inv_val X).
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 ; (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.
       (pr1 x × r) ; split.
      rewrite <- isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, islunit_oneNonnegativeRationals.
      reflexivity.
      exact (pr2 (pr2 x)).
      apply hinhpr.
       (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.
       (pr1 l) ; repeat split.
      intros s Xs.
      rewrite (iscomm_multNonnegativeRationals (/ pr1 x)%NRat), isassoc_multNonnegativeRationals.
      apply (pr1 (pr2 l)).
      unfold Y ; apply hinhpr.
      now 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 ; 0%NRat ; split.
  now rewrite israbsorb_zero_multNonnegativeRationals.
  exact X_0.
  exact Y_1.
Qed.

End Dcuts_inv'.

Definition Dcuts_inv (X : Dcuts) (X_0 : X 0) : Dcuts.
Proof.
  intros.
  apply (make_Dcuts (Dcuts_inv_val (pr1 X))).
  - now apply Dcuts_inv_bot.
  - apply Dcuts_inv_open.
    now apply is_Dcuts_bot.
    now apply Dcuts_def_corr_finite, is_Dcuts_corr.
  - apply Dcuts_inv_corr.
    now apply is_Dcuts_bot.
    now apply is_Dcuts_open.
    now apply is_Dcuts_corr.
    now apply_pr2 Dcuts_apzero_notempty.
Defined.

Algebraic properties


Lemma Dcuts_NQmult_mult :
   (x : NonnegativeRationals) (y : Dcuts) (Hx0 : (0 < x)%NRat), Dcuts_NQmult x y Hx0 = Dcuts_mult (NonnegativeRationals_to_Dcuts x) y.
Proof.
  intros x y Hx0.
  apply Dcuts_eq_is_eq.
  intros r ; split.
  - apply hinhuniv.
    intros ry.
    generalize (is_Dcuts_open _ _ (pr2 (pr2 ry))).
    apply hinhfun ; intros ry'.
     (((x × (pr1 ry)) / (pr1 ry'))%NRat,, (pr1 ry')).
    simpl.
    assert (Hry' : (0 < pr1 ry')%NRat).
    { eapply istrans_le_lt_ltNonnegativeRationals, (pr2 (pr2 ry')).
      apply isnonnegative_NonnegativeRationals. }
    split ; [ | split].
    + unfold divNonnegativeRationals.
      rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, isrunit_oneNonnegativeRationals.
      exact (pr1 (pr2 ry)).
      exact Hry'.
    + pattern x at 2.
      rewrite <- (isrunit_oneNonnegativeRationals x).
      unfold divNonnegativeRationals.
      rewrite isassoc_multNonnegativeRationals.
      apply multNonnegativeRationals_ltcompat_l.
      exact Hx0.
      rewrite <- (isrinv_NonnegativeRationals (pr1 ry')).
      apply multNonnegativeRationals_ltcompat_r.
      apply ispositive_invNonnegativeRationals.
      exact Hry'.
      exact (pr2 (pr2 ry')).
      exact Hry'.
    + exact (pr1 (pr2 ry')).
  - apply hinhfun ; simpl.
    intros xy.
     (pr1 (pr1 xy) × pr2 (pr1 xy) / x).
    split.
    + rewrite iscomm_multNonnegativeRationals.
      unfold divNonnegativeRationals.
      rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, isrunit_oneNonnegativeRationals.
      exact (pr1 (pr2 xy)).
      exact Hx0.
    + apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 xy))).
      pattern (pr2 (pr1 xy)) at 2.
      rewrite <- (isrunit_oneNonnegativeRationals (pr2 (pr1 xy))), <- (isrinv_NonnegativeRationals x), <- isassoc_multNonnegativeRationals.
      apply multNonnegativeRationals_lecompat_r.
      rewrite iscomm_multNonnegativeRationals.
      apply multNonnegativeRationals_lecompat_l.
      apply lt_leNonnegativeRationals.
      exact (pr1 (pr2 (pr2 xy))).
      exact Hx0.
Qed.

Lemma iscomm_Dcuts_plus : iscomm Dcuts_plus.
Proof.
  assert (H : x y, x0 : NonnegativeRationals, x0 Dcuts_plus x y x0 Dcuts_plus y x).
  { intros x y r.
    apply hinhuniv, sumofmaps ; simpl pr1.
    - apply sumofmaps ; intros Hr.
      + now apply hinhpr ; left ; right.
      + now apply hinhpr ; left ; left.
    - intros xy.
      apply hinhpr ; right ; (pr2 (pr1 xy),, pr1 (pr1 xy)).
      repeat split.
      + pattern r at 1 ; rewrite (pr1 (pr2 xy)).
        apply iscomm_plusNonnegativeRationals.
      + exact (pr2 (pr2 (pr2 xy))).
      + exact (pr1 (pr2 (pr2 xy))).
  }
  intros x y.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - now apply H.
  - now apply H.
Qed.

Lemma Dcuts_plus_lt_l :
   x x' y : Dcuts, Dcuts_plus x y < Dcuts_plus x' y x < x'.
Proof.
  intros x x' y.
  apply hinhuniv ; intros r.
  generalize (pr2 (pr2 r)) ; apply hinhfun ; apply sumofmaps ;
  [ apply sumofmaps ; [ intros Xr | intros Yr] | intros xy ].
  - (pr1 r) ; split.
    intro H ; apply (pr1 (pr2 r)).
    now apply hinhpr ; left ; left.
    exact Xr.
  - apply fromempty, (pr1 (pr2 r)).
    now apply hinhpr ; left ; right.
  - (pr1 (pr1 xy)) ; split.
    intro H ; apply (pr1 (pr2 r)).
    apply hinhpr ; right ; (pr1 xy).
    repeat split.
    exact (pr1 (pr2 xy)).
    exact H.
    exact (pr2 (pr2 (pr2 xy))).
    exact (pr1 (pr2 (pr2 xy))).
Qed.

Lemma islapbinop_Dcuts_plus : islapbinop Dcuts_plus.
Proof.
  intros y x x'.
  apply sumofmaps ; intros Hlt.
  - left.
    now apply Dcuts_plus_lt_l with y.
  - right.
    now apply Dcuts_plus_lt_l with y.
Qed.
Lemma israpbinop_Dcuts_plus : israpbinop Dcuts_plus.
Proof.
  intros x y y'.
  rewrite !(iscomm_Dcuts_plus x).
  now apply islapbinop_Dcuts_plus.
Qed.

Lemma iscomm_Dcuts_mult : iscomm Dcuts_mult.
Proof.
  intros x y.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - apply hinhfun. intros xy.
     (pr2 (pr1 xy),, pr1 (pr1 xy)) ; repeat split.
    rewrite iscomm_multNonnegativeRationals.
    exact (pr1 (pr2 xy)).
    exact (pr2 (pr2 (pr2 xy))).
    exact (pr1 (pr2 (pr2 xy))).
  - apply hinhfun ; intros xy.
     (pr2 (pr1 xy),, pr1 (pr1 xy)) ; repeat split.
    rewrite iscomm_multNonnegativeRationals.
    exact (pr1 (pr2 xy)).
    exact (pr2 (pr2 (pr2 xy))).
    exact (pr1 (pr2 (pr2 xy))).
Qed.

Lemma Dcuts_mult_lt_l :
   x x' y : Dcuts, Dcuts_mult x y < Dcuts_mult x' y x < x'.
Proof.
  intros x x' y.
  apply hinhuniv ; intros r.
  generalize (pr2 (pr2 r)).
  apply hinhfun ; intros xy.
   (pr1 (pr1 xy)) ; split.
  intro H ; apply (pr1 (pr2 r)).
  apply hinhpr ; (pr1 xy).
  repeat split.
  exact (pr1 (pr2 xy)).
  exact H.
  exact (pr2 (pr2 (pr2 xy))).
  exact (pr1 (pr2 (pr2 xy))).
Qed.
Lemma islapbinop_Dcuts_mult : islapbinop Dcuts_mult.
Proof.
  intros y x x'.
  apply sumofmaps.
  intros Hlt.
  - left.
    now apply Dcuts_mult_lt_l with y.
  - right.
    now apply Dcuts_mult_lt_l with y.
Qed.
Lemma israpbinop_Dcuts_mult : israpbinop Dcuts_mult.
Proof.
  intros x y y'.
  rewrite !(iscomm_Dcuts_mult x).
  now apply islapbinop_Dcuts_mult.
Qed.

Lemma isassoc_Dcuts_plus : isassoc Dcuts_plus.
Proof.
  intros x y z.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - apply hinhuniv, sumofmaps ; simpl pr1.
    + apply sumofmaps.
      × apply hinhuniv, sumofmaps.
        { apply sumofmaps ; intros Hr.
          - now apply hinhpr ; left ; left.
          - apply hinhpr ; left ; right.
            now apply hinhpr ; left ; left. }
        { intros xy.
          apply hinhpr ; right ; (pr1 xy).
          repeat split.
          - exact (pr1 (pr2 xy)).
          - exact (pr1 (pr2 (pr2 xy))).
          - apply hinhpr ; left ; left.
            exact (pr2 (pr2 (pr2 xy))). }
      × intros Hr.
        apply hinhpr ; left ; right.
        now apply hinhpr ; left ; right.
    + intros xyz.
      generalize (pr1 (pr2 (pr2 xyz))) ; apply hinhuniv, sumofmaps.
      × apply sumofmaps ; intros Hxy.
        { apply hinhpr ; right ; (pr1 xyz).
          repeat split.
          - exact (pr1 (pr2 xyz)).
          - exact Hxy.
          - apply hinhpr ; left ; right.
            exact (pr2 (pr2 (pr2 xyz))). }
        { apply hinhpr ; left ; right.
          apply hinhpr ; right ; (pr1 xyz).
          repeat split.
          - exact (pr1 (pr2 xyz)).
          - exact Hxy.
          - exact (pr2 (pr2 (pr2 xyz))). }
      × intros xy.
        apply hinhpr ; right ; (pr1 (pr1 xy),,pr2 (pr1 xy) + pr2 (pr1 xyz)).
        repeat split ; simpl.
        { pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 xy)).
          now apply isassoc_plusNonnegativeRationals. }
        { exact (pr1 (pr2 (pr2 xy))). }
        { apply hinhpr ; right ; (pr2 (pr1 xy),,pr2 (pr1 xyz)).
          repeat split.
          - exact (pr2 (pr2 (pr2 xy))).
          - exact (pr2 (pr2 (pr2 xyz))). }
  - apply hinhuniv, sumofmaps.
    + apply sumofmaps.
      × intros Hr.
        apply hinhpr ; left ; left.
        now apply hinhpr ; left ; left.
      × apply hinhuniv, sumofmaps.
        { apply sumofmaps ; intros Hr.
          - apply hinhpr ; left ; left.
            now apply hinhpr ; left ; right.
          - now apply hinhpr ; left ; right. }
        { intros yz ; simpl in × |-.
          apply hinhpr ; right ; (pr1 yz).
          repeat split.
          - exact (pr1 (pr2 yz)).
          - apply hinhpr ; left ; right.
            exact (pr1 (pr2 (pr2 yz))).
          - exact (pr2 (pr2 (pr2 yz))). }
    + intros xyz.
      generalize (pr2 (pr2 (pr2 xyz))) ; apply hinhuniv, sumofmaps.
      × apply sumofmaps ; intros Hyz.
        { apply hinhpr ; left ; left.
          apply hinhpr ; right ; (pr1 xyz).
          repeat split.
          - exact (pr1 (pr2 xyz)).
          - exact (pr1 (pr2 (pr2 xyz))).
          - exact Hyz. }
        { apply hinhpr ; right ; (pr1 xyz).
          repeat split.
          - exact (pr1 (pr2 xyz)).
          - apply hinhpr ; left ; left.
            exact (pr1 (pr2 (pr2 xyz))).
          - exact Hyz. }
      × intros yz.
        apply hinhpr ; right ; ((pr1 (pr1 xyz)+ pr1 (pr1 yz),, pr2 (pr1 yz))).
        repeat split ; simpl.
        { pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 yz)).
          now rewrite isassoc_plusNonnegativeRationals. }
        { apply hinhpr ; right ; (pr1 (pr1 xyz),,(pr1 (pr1 yz))).
          repeat split.
          - exact (pr1 (pr2 (pr2 xyz))).
          - exact (pr1 (pr2 (pr2 yz))). }
        { exact (pr2 (pr2 (pr2 yz))). }
Qed.
Lemma islunit_Dcuts_plus_zero : islunit Dcuts_plus 0.
Proof.
  intros x.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - apply hinhuniv, sumofmaps.
    + apply sumofmaps ; intro Hr.
      × now apply Dcuts_zero_empty in Hr.
      × exact Hr.
    + intros x0.
      apply fromempty.
      exact (Dcuts_zero_empty _ (pr1 (pr2 (pr2 x0)))).
  - intros Hr.
    now apply hinhpr ; left ; right.
Qed.
Lemma isrunit_Dcuts_plus_zero : isrunit Dcuts_plus 0.
Proof.
  intros x.
  rewrite iscomm_Dcuts_plus.
  now apply islunit_Dcuts_plus_zero.
Qed.
Lemma isassoc_Dcuts_mult : isassoc Dcuts_mult.
Proof.
  intros x y z.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - apply hinhuniv ; intros xyz.
    generalize (pr1 (pr2 (pr2 xyz))).
    apply hinhfun ; intros xy.
    pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 xy)), isassoc_multNonnegativeRationals.
     (pr1 (pr1 xy),,(pr2 (pr1 xy) × pr2 (pr1 xyz))) ; simpl ; repeat split.
    + exact (pr1 (pr2 (pr2 xy))).
    + apply hinhpr ; (pr2 (pr1 xy),,pr2 (pr1 (xyz))).
      repeat split.
      exact (pr2 (pr2 (pr2 xy))).
      exact (pr2 (pr2 (pr2 xyz))).
  - apply hinhuniv ; intros xyz.
    generalize (pr2 (pr2 (pr2 xyz))).
    apply hinhfun ; intros yz.
    pattern r at 1 ; rewrite (pr1 (pr2 xyz)), (pr1 (pr2 yz)), <- isassoc_multNonnegativeRationals.
     ((pr1 (pr1 xyz) × pr1 (pr1 yz)) ,, pr2 (pr1 yz)) ; simpl ; repeat split.
    + apply hinhpr ; (pr1 (pr1 xyz),,pr1 (pr1 yz)).
      repeat split.
      exact (pr1 (pr2 (pr2 xyz))).
      exact (pr1 (pr2 (pr2 yz))).
    + exact (pr2 (pr2 (pr2 yz))).
Qed.
Lemma islunit_Dcuts_mult_one : islunit Dcuts_mult Dcuts_one.
Proof.
  intros x.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - apply hinhuniv ; intros ix.
    apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 ix))).
    pattern r at 1 ; rewrite (pr1 (pr2 ix)), iscomm_multNonnegativeRationals.
    apply multNonnegativeRationals_le1_r, lt_leNonnegativeRationals.
    exact (pr1 (pr2 (pr2 ix))).
  - intros Xr.
    generalize (is_Dcuts_open x r Xr).
    apply hinhfun ; intros q.
     ((r/pr1 q)%NRat,,pr1 q) ; repeat split.
    + simpl.
      rewrite iscomm_multNonnegativeRationals, multdivNonnegativeRationals.
      reflexivity.
      apply istrans_le_lt_ltNonnegativeRationals with (2 := pr2 (pr2 q)).
      apply isnonnegative_NonnegativeRationals.
    + change (r / pr1 q < 1)%NRat.
       apply_pr2 (multNonnegativeRationals_ltcompat_l (pr1 q)).
       apply istrans_le_lt_ltNonnegativeRationals with (2 := pr2 (pr2 q)).
       apply isnonnegative_NonnegativeRationals.
       rewrite multdivNonnegativeRationals, isrunit_oneNonnegativeRationals.
       exact (pr2 (pr2 q)).
       apply istrans_le_lt_ltNonnegativeRationals with (2 := pr2 (pr2 q)).
       apply isnonnegative_NonnegativeRationals.
    + exact (pr1 (pr2 q)).
Qed.
Lemma isrunit_Dcuts_mult_one : isrunit Dcuts_mult Dcuts_one.
Proof.
  intros x.
  rewrite iscomm_Dcuts_mult.
  now apply islunit_Dcuts_mult_one.
Qed.
Lemma islabsorb_Dcuts_mult_zero :
   x : Dcuts, Dcuts_mult Dcuts_zero x = Dcuts_zero.
Proof.
  intros x.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - apply hinhuniv ; intros ix.
    apply fromempty.
    now apply (Dcuts_zero_empty _ (pr1 (pr2 (pr2 ix)))).
  - intro Hr.
    now apply Dcuts_zero_empty in Hr.
Qed.
Lemma israbsorb_Dcuts_mult_zero :
   x : Dcuts, Dcuts_mult x Dcuts_zero = Dcuts_zero.
Proof.
  intros x.
  rewrite iscomm_Dcuts_mult.
  now apply islabsorb_Dcuts_mult_zero.
Qed.
Lemma isldistr_Dcuts_plus_mult : isldistr Dcuts_plus Dcuts_mult.
Proof.
  intros x y z.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - apply hinhuniv ; intros xyz.
    rewrite (pr1 (pr2 xyz)).
    generalize (pr2 (pr2 (pr2 xyz))).
    apply hinhfun ; apply sumofmaps ;
    [ apply sumofmaps ; [intros Xr | intros Yr]
    | intros xy ].
    + left ; left ; apply hinhpr.
       (pr1 xyz) ; repeat split.
      exact (pr1 (pr2 (pr2 xyz))).
      exact Xr.
    + left ; right ; apply hinhpr.
       (pr1 xyz) ; repeat split.
      exact (pr1 (pr2 (pr2 xyz))).
      exact Yr.
    + rewrite (pr1 (pr2 xy)), isldistr_mult_plusNonnegativeRationals.
      right ;
         (pr1 (pr1 xyz) × pr1 (pr1 xy),, pr1 (pr1 xyz) × pr2 (pr1 xy)) ; repeat split.
      × apply hinhpr ; (pr1 (pr1 xyz),,pr1 (pr1 xy)).
        repeat split.
        exact (pr1 (pr2 (pr2 xyz))).
        exact (pr1 (pr2 (pr2 xy))).
      × apply hinhpr ; (pr1 (pr1 xyz),,pr2 (pr1 xy)).
        repeat split.
        exact (pr1 (pr2 (pr2 xyz))).
        exact (pr2 (pr2 (pr2 xy))).
  - apply hinhuniv ; apply sumofmaps ;
    [ apply sumofmaps | intros zxzy ].
    + apply hinhfun ; intros zx.
      rewrite (pr1 (pr2 zx)).
       (pr1 zx) ; repeat split.
      × exact (pr1 (pr2 (pr2 zx))).
      × apply hinhpr ; left ; left.
        exact (pr2 (pr2 (pr2 zx))).
    + apply hinhfun ; intros zy.
      rewrite (pr1 (pr2 zy)).
       (pr1 zy) ; repeat split.
      × exact (pr1 (pr2 (pr2 zy))).
      × apply hinhpr ; left ; right.
        exact (pr2 (pr2 (pr2 zy))).
    + rewrite (pr1 (pr2 zxzy)).
      generalize (pr1 (pr2 (pr2 zxzy))) (pr2 (pr2 (pr2 zxzy))).
      apply hinhfun2 ; intros zx zy.
      rewrite (pr1 (pr2 zx)), (pr1 (pr2 zy)).
      generalize (isdecrel_leNonnegativeRationals (NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy))) 0%NRat) ;
        apply sumofmaps ; [intros Heq| intros Hlt].
      apply NonnegativeRationals_eq0_le0 in Heq.
      × apply NQmax_eq_zero in Heq.
        rewrite (pr1 Heq), (pr2 Heq).
         (0%NRat,,pr2 (pr1 zx)) ; simpl ; repeat split.
        rewrite !islabsorb_zero_multNonnegativeRationals.
        now apply isrunit_zeroNonnegativeRationals.
        apply (is_Dcuts_bot _ _ (pr1 (pr2 (pr2 zx)))).
        apply isnonnegative_NonnegativeRationals.
        apply hinhpr ; left ; left.
        exact (pr2 (pr2 (pr2 zx))).
      × apply notge_ltNonnegativeRationals in Hlt.
         (NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy)),, (pr1 (pr1 zx) × pr2 (pr1 zx) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy)) + (pr1 (pr1 zy) × pr2 (pr1 zy) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy))))) ;
          simpl ; repeat split.
        unfold divNonnegativeRationals.
        rewrite <- isrdistr_mult_plusNonnegativeRationals.
        now apply pathsinv0, multdivNonnegativeRationals.
        apply NQmax_case.
        exact (pr1 (pr2 (pr2 zx))).
        exact (pr1 (pr2 (pr2 zy))).
        apply hinhpr ; right.
         (pr1 (pr1 zx) × pr2 (pr1 zx) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy)) ,,
   pr1 (pr1 zy) × pr2 (pr1 zy) / NQmax (pr1 (pr1 zx)) (pr1 (pr1 zy))) ; simpl ; repeat split.
        apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 zx))).
        rewrite iscomm_multNonnegativeRationals.
        unfold divNonnegativeRationals ;
          rewrite isassoc_multNonnegativeRationals.
        apply multNonnegativeRationals_le1_r, divNonnegativeRationals_le1.
        now apply NQmax_le_l.
        apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 zy))).
        rewrite iscomm_multNonnegativeRationals.
        unfold divNonnegativeRationals ;
          rewrite isassoc_multNonnegativeRationals.
        apply multNonnegativeRationals_le1_r, divNonnegativeRationals_le1.
        now apply NQmax_le_r.
Qed.
Lemma isrdistr_Dcuts_plus_mult : isrdistr Dcuts_plus Dcuts_mult.
Proof.
  intros x y z.
  rewrite <- ! (iscomm_Dcuts_mult z).
  now apply isldistr_Dcuts_plus_mult.
Qed.

Lemma Dcuts_ap_one_zero : 1 0.
Proof.
  apply isapfun_NonnegativeRationals_to_Dcuts'.
  apply gtNonnegativeRationals_noteq.
  exact ispositive_oneNonnegativeRationals.
Qed.
Definition islinv_Dcuts_inv :
   x : Dcuts, Hx0 : x 0, Dcuts_mult (Dcuts_inv x Hx0) x = 1.
Proof.
  intros x Hx0.
  apply Dcuts_eq_is_eq ; intros q ; split.
  - apply hinhuniv ; intros xy.
    rewrite (pr1 (pr2 xy)).
    generalize (pr1 (pr2 (pr2 xy))).
    apply hinhuniv ; intros l.
    change (pr1 (pr1 xy) × pr2 (pr1 xy) < 1)%NRat.
    apply istrans_le_lt_ltNonnegativeRationals with (pr1 l).
    apply (pr1 (pr2 l)).
    exact (pr2 (pr2 (pr2 xy))).
    exact (pr2 (pr2 (pr2 l))).
  - change (q 1) with (q < 1)%NRat ; intro Hq.
    generalize Hx0 ; intro Hx.
    apply_pr2_in Dcuts_apzero_notempty Hx0.
    generalize (eq0orgt0NonnegativeRationals q) ; apply sumofmaps ; intros Hq0.
    + rewrite Hq0.
      apply hinhpr.
       (0%NRat,,0%NRat) ; repeat split.
      × simpl ; now rewrite islabsorb_zero_multNonnegativeRationals.
      × apply hinhpr.
         (/ 2)%NRat ; split.
        simpl pr1 ; intros.
        rewrite islabsorb_zero_multNonnegativeRationals.
        now apply isnonnegative_NonnegativeRationals.
        split.
        apply (pr1 (ispositive_invNonnegativeRationals _)).
        exact ispositive_twoNonnegativeRationals.
        apply_pr2 (multNonnegativeRationals_ltcompat_l 2%NRat).
        exact ispositive_twoNonnegativeRationals.
        rewrite isrunit_oneNonnegativeRationals, isrinv_NonnegativeRationals.
        exact one_lt_twoNonnegativeRationals.
        exact ispositive_twoNonnegativeRationals.
      × exact Hx0.
    + generalize (is_Dcuts_open _ _ Hx0).
      apply hinhuniv ; intros r.
      apply between_ltNonnegativeRationals in Hq.
      rename Hq into t.
      set (c := pr1 r × (/ pr1 t - 1)%NRat).
      assert (Hc0 : (0 < c)%NRat).
      { unfold c.
        apply ispositive_multNonnegativeRationals.
        exact (pr2 (pr2 r)).
        apply ispositive_minusNonnegativeRationals.
        apply_pr2 (multNonnegativeRationals_ltcompat_l (pr1 t)).
        apply istrans_ltNonnegativeRationals with q.
        exact Hq0.
        exact (pr1 (pr2 t)).
        rewrite isrunit_oneNonnegativeRationals, isrinv_NonnegativeRationals.
        exact (pr2 (pr2 t)).
        apply istrans_ltNonnegativeRationals with q.
        exact Hq0.
        exact (pr1 (pr2 t)). }
      generalize (Dcuts_def_corr_not_empty _ Hx0 (is_Dcuts_corr x) _ Hc0).
      apply hinhfun ; intros r'.
       ((q × / (NQmax (pr1 r) (pr1 r')))%NRat,,NQmax (pr1 r) (pr1 r')) ; repeat split.
      × simpl.
        rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, isrunit_oneNonnegativeRationals.
        reflexivity.
        apply istrans_lt_le_ltNonnegativeRationals with (pr1 r).
        exact (pr2 (pr2 r)).
        now apply NQmax_le_l.
      × apply hinhpr ; simpl pr1.
         (q / NQmax (pr1 r) (pr1 r') × (NQmax (pr1 r) (pr1 r') + c))%NRat.
        repeat split.
        intros rx Xrx.
        apply multNonnegativeRationals_lecompat_l, lt_leNonnegativeRationals.
        apply (Dcuts_finite x).
        intro H ; apply (pr2 (pr2 r')).
        apply is_Dcuts_bot with (1 := H).
        now apply plusNonnegativeRationals_lecompat_r ; apply NQmax_le_r.
        exact Xrx.
        apply ispositive_multNonnegativeRationals.
        apply ispositive_divNonnegativeRationals.
        exact Hq0.
        apply istrans_lt_le_ltNonnegativeRationals with (pr1 r).
        exact (pr2 (pr2 r)).
        now apply NQmax_le_l.
        rewrite iscomm_plusNonnegativeRationals.
        now apply ispositive_plusNonnegativeRationals_l.
        unfold divNonnegativeRationals.
        apply_pr2 (multNonnegativeRationals_ltcompat_l (/ q)%NRat).
        now apply ispositive_invNonnegativeRationals.
        rewrite isrunit_oneNonnegativeRationals, <- !isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, islunit_oneNonnegativeRationals.
        2: exact Hq0.
        apply_pr2 (multNonnegativeRationals_ltcompat_l (NQmax (pr1 r) (pr1 r'))).
        apply istrans_lt_le_ltNonnegativeRationals with (pr1 r).
        exact (pr2 (pr2 r)).
        now apply NQmax_le_l.
        rewrite <- !isassoc_multNonnegativeRationals, isrinv_NonnegativeRationals, islunit_oneNonnegativeRationals.
        2: apply istrans_lt_le_ltNonnegativeRationals with (pr1 r).
        2: exact (pr2 (pr2 r)).
        2: now apply NQmax_le_l.
        apply (minusNonnegativeRationals_ltcompat_l' _ _ (NQmax (pr1 r) (pr1 r') × 1)%NRat).
        rewrite <- isldistr_mult_minusNonnegativeRationals, isrunit_oneNonnegativeRationals, plusNonnegativeRationals_minus_l.
        unfold c.
        apply multNonnegativeRationals_le_lt.
        exact (pr2 (pr2 r)).
        now apply NQmax_le_l.
        apply_pr2 (multNonnegativeRationals_ltcompat_l q).
        exact Hq0.
        rewrite !isldistr_mult_minusNonnegativeRationals, isrinv_NonnegativeRationals, isrunit_oneNonnegativeRationals.
        2: exact Hq0.
        apply_pr2 (multNonnegativeRationals_ltcompat_r (pr1 t)).
        apply istrans_ltNonnegativeRationals with q.
        exact Hq0.
        exact (pr1 (pr2 t)).
        rewrite !isrdistr_mult_minusNonnegativeRationals, isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, isrunit_oneNonnegativeRationals, islunit_oneNonnegativeRationals.
        2: apply istrans_ltNonnegativeRationals with q.
        apply minusNonnegativeRationals_ltcompat_l.
        exact (pr1 (pr2 t)).
        pattern t at 1 ;
          rewrite <- (islunit_oneNonnegativeRationals (pr1 t)).
        apply multNonnegativeRationals_ltcompat_r.
        apply istrans_ltNonnegativeRationals with q.
        exact Hq0.
        exact (pr1 (pr2 t)).
        apply istrans_ltNonnegativeRationals with (pr1 t).
        exact (pr1 (pr2 t)).
        exact (pr2 (pr2 t)).
        exact Hq0.
        exact (pr1 (pr2 t)).
      × simpl.
        apply NQmax_case.
        exact (pr1 (pr2 r)).
        exact (pr1 (pr2 r')).
Qed.
Lemma isrinv_Dcuts_inv :
   x : Dcuts, Hx0 : x 0, Dcuts_mult x (Dcuts_inv x Hx0) = 1.
Proof.
  intros x Hx0.
  rewrite iscomm_Dcuts_mult.
  now apply islinv_Dcuts_inv.
Qed.

Lemma Dcuts_plus_ltcompat_l :
   x y z: Dcuts, (y < z) (Dcuts_plus y x < Dcuts_plus z x).
Proof.
  intros x y z.
  split.
  - apply hinhuniv ; intros r.
    generalize (is_Dcuts_open _ _ (pr2 (pr2 r))) ; apply hinhuniv ; intros r'.
    generalize (pr1 r') (pr1 (pr2 r')) (pr2 (pr2 r')) ; clear r' ; intros r' Zr' Hr.
    apply ispositive_minusNonnegativeRationals in Hr.
    generalize (is_Dcuts_corr x _ Hr).
    apply hinhuniv ; apply sumofmaps ; [intros nXc | ].
    + apply hinhpr ; r' ; split.
      × unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ;
        [apply sumofmaps ; [intros Yr' | intros Xr'] | intros yx ].
        apply (pr1 (pr2 r)), is_Dcuts_bot with (1 := Yr'), lt_leNonnegativeRationals.
        now apply_pr2 ispositive_minusNonnegativeRationals.
        apply nXc, is_Dcuts_bot with (1 := Xr'), minusNonnegativeRationals_le.
        generalize (pr1 (pr2 yx)) ; apply gtNonnegativeRationals_noteq.
        pattern r' at 1 ; rewrite <- (minusNonnegativeRationals_plus_r (pr1 r) r'), iscomm_plusNonnegativeRationals.
        apply plusNonnegativeRationals_ltcompat.
        apply (Dcuts_finite y).
        exact (pr1 (pr2 r)).
        exact (pr1 (pr2 (pr2 yx))).
        apply (Dcuts_finite x).
        exact nXc.
        exact (pr2 (pr2 (pr2 yx))).
        apply lt_leNonnegativeRationals.
        now apply_pr2 ispositive_minusNonnegativeRationals.
      × now apply hinhpr ; left ; left.
    + intros q.
      generalize (pr1 q) (pr1 (pr2 q)) (pr2 (pr2 q)) ;
        clear q ;
        intros q Xq nXq.
      apply hinhpr.
       (r' + q)%NRat ; split.
      × unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ; [ apply sumofmaps ; [ intros Yr' | intros Xr'] | intros yx ].
        apply (pr1 (pr2 r)), is_Dcuts_bot with (1 := Yr'), lt_leNonnegativeRationals.
        rewrite <- (isrunit_zeroNonnegativeRationals (pr1 r)).
        apply plusNonnegativeRationals_lt_le_ltcompat.
        now apply_pr2 ispositive_minusNonnegativeRationals.
        now apply isnonnegative_NonnegativeRationals.
        apply nXq, is_Dcuts_bot with (1 := Xr').
        rewrite iscomm_plusNonnegativeRationals.
        apply plusNonnegativeRationals_lecompat_r.
        now apply minusNonnegativeRationals_le.
        generalize (pr1 (pr2 yx)) ; apply gtNonnegativeRationals_noteq.
        pattern (r' + q) at 1 ;
          rewrite (iscomm_plusNonnegativeRationals r' q).
        pattern r' at 1 ;
          rewrite <- (minusNonnegativeRationals_plus_r (pr1 r) r'), <- isassoc_plusNonnegativeRationals, iscomm_plusNonnegativeRationals.
        apply plusNonnegativeRationals_ltcompat.
        apply (Dcuts_finite y).
        exact (pr1 (pr2 r)).
        exact (pr1 (pr2 (pr2 yx))).
        apply (Dcuts_finite x).
        exact nXq.
        exact (pr2 (pr2 (pr2 yx))).
        apply lt_leNonnegativeRationals.
        now apply_pr2 ispositive_minusNonnegativeRationals.
      × apply hinhpr ; right ; (r',,q) ; repeat split.
        exact Zr'.
        exact Xq.
  - now apply Dcuts_plus_lt_l.
Qed.
Lemma Dcuts_plus_lecompat_l :
   x y z: Dcuts, (y z) (Dcuts_plus y x Dcuts_plus z x).
Proof.
  intros x y z.
  split.
  - intros H ; apply Dcuts_nlt_ge ; intro H0 ; apply (pr2 (Dcuts_nlt_ge _ _) H).
    now apply_pr2 (Dcuts_plus_ltcompat_l x).
  - intros H ; apply Dcuts_nlt_ge ; intro H0 ; apply (pr2 (Dcuts_nlt_ge _ _) H).
    now apply Dcuts_plus_ltcompat_l.
Qed.
Lemma Dcuts_plus_ltcompat_r :
   x y z: Dcuts, (y < z) (Dcuts_plus x y < Dcuts_plus x z).
Proof.
  intros x y z.
  rewrite ! (iscomm_Dcuts_plus x).
  now apply Dcuts_plus_ltcompat_l.
Qed.
Lemma Dcuts_plus_lecompat_r :
   x y z: Dcuts, (y z) (Dcuts_plus x y Dcuts_plus x z).
Proof.
  intros x y z.
  rewrite ! (iscomm_Dcuts_plus x).
  now apply Dcuts_plus_lecompat_l.
Qed.

Lemma Dcuts_plus_le_l :
   x y, x Dcuts_plus x y.
Proof.
  intros x y r Xr.
  now apply hinhpr ; left ; left.
Qed.
Lemma Dcuts_plus_le_r :
   x y, y Dcuts_plus x y.
Proof.
  intros x y r Xr.
  now apply hinhpr ; left ; right.
Qed.

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 ; 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 ; (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'.
     (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 ; (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.
Lemma Dcuts_mult_ltcompat_l' :
   x y z: Dcuts, (Dcuts_mult y x < Dcuts_mult z x) (y < z).
Proof.
  intros x y z.
  now apply Dcuts_mult_lt_l.
Qed.
Lemma Dcuts_mult_lecompat_l :
   x y z: Dcuts, (0 < x) (Dcuts_mult y x Dcuts_mult z x) (y z).
Proof.
  intros x y z Hx0.
  intros H ; apply Dcuts_nlt_ge ; intro H0 ; apply (pr2 (Dcuts_nlt_ge _ _) H).
  now apply Dcuts_mult_ltcompat_l.
Qed.
Lemma Dcuts_mult_lecompat_l' :
   x y z: Dcuts, (y z) (Dcuts_mult y x Dcuts_mult z x).
Proof.
  intros x y z.
  intros H ; apply Dcuts_nlt_ge ; intro H0 ; apply (pr2 (Dcuts_nlt_ge _ _) H).
  now apply (Dcuts_mult_ltcompat_l' x).
Qed.

Lemma Dcuts_mult_ltcompat_r :
   x y z: Dcuts, (0 < x) (y < z) (Dcuts_mult x y < Dcuts_mult x z).
Proof.
  intros x y z.
  rewrite ! (iscomm_Dcuts_mult x).
  now apply Dcuts_mult_ltcompat_l.
Qed.
Lemma Dcuts_mult_ltcompat_r' :
   x y z: Dcuts, (Dcuts_mult x y < Dcuts_mult x z) (y < z).
Proof.
  intros x y z.
  rewrite ! (iscomm_Dcuts_mult x).
  now apply Dcuts_mult_ltcompat_l'.
Qed.
Lemma Dcuts_mult_lecompat_r :
   x y z: Dcuts, (0 < x) (Dcuts_mult x y Dcuts_mult x z) (y z).
Proof.
  intros x y z.
  rewrite ! (iscomm_Dcuts_mult x).
  now apply Dcuts_mult_lecompat_l.
Qed.
Lemma Dcuts_mult_lecompat_r' :
   x y z: Dcuts, (y z) (Dcuts_mult x y Dcuts_mult x z).
Proof.
  intros x y z.
  rewrite ! (iscomm_Dcuts_mult x).
  now apply Dcuts_mult_lecompat_l'.
Qed.

Lemma Dcuts_plus_double :
   x : Dcuts, Dcuts_plus x x = Dcuts_mult Dcuts_two x.
Proof.
  intros x.
  rewrite <- (Dcuts_NQmult_mult _ _ ispositive_twoNonnegativeRationals).
  apply Dcuts_eq_is_eq.
  intros r ; split.
  - apply hinhfun ; apply sumofmaps ; [ apply sumofmaps ; intros Xr | intros xy ; rewrite (pr1 (pr2 xy))].
    + (r / 2)%NRat.
      simpl ; split.
      × apply pathsinv0, multdivNonnegativeRationals.
        exact ispositive_twoNonnegativeRationals.
      × apply is_Dcuts_bot with (1 := Xr).
        pattern r at 2 ; rewrite (NQhalf_double r).
        apply plusNonnegativeRationals_le_l.
    + (r / 2)%NRat.
      simpl ; split.
      × apply pathsinv0, multdivNonnegativeRationals.
        exact ispositive_twoNonnegativeRationals.
      × apply is_Dcuts_bot with (1 := Xr).
        pattern r at 2 ; rewrite (NQhalf_double r).
        apply plusNonnegativeRationals_le_l.
    + ((pr1 (pr1 xy) + pr2 (pr1 xy)) / 2)%NRat.
      split.
      × apply pathsinv0, multdivNonnegativeRationals.
        exact ispositive_twoNonnegativeRationals.
      × generalize (isdecrel_ltNonnegativeRationals (pr1 (pr1 xy)) (pr2 (pr1 xy))) ; apply sumofmaps ; intros H.
        apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 xy))).
        pattern (pr2 (pr1 xy)) at 2 ; rewrite (NQhalf_double (pr2 (pr1 xy))).
        unfold divNonnegativeRationals.
        rewrite isrdistr_mult_plusNonnegativeRationals.
        apply plusNonnegativeRationals_lecompat_r.
        apply multNonnegativeRationals_lecompat_r.
        now apply lt_leNonnegativeRationals.
        apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 xy))).
        pattern (pr1 (pr1 xy)) at 2 ; rewrite (NQhalf_double (pr1 (pr1 xy))).
        unfold divNonnegativeRationals.
        rewrite isrdistr_mult_plusNonnegativeRationals.
        apply plusNonnegativeRationals_lecompat_l.
        apply multNonnegativeRationals_lecompat_r.
        now apply notlt_geNonnegativeRationals.
  - apply hinhfun ; intros q ; rewrite (pr1 (pr2 q)).
    right.
     (pr1 q,,pr1 q).
    repeat split.
    + assert (X : (2 = 1+1)%NRat).
      { apply subtypePath_prop ; simpl.
        apply hq2eq1plus1. }
      pattern 2%NRat at 1 ; rewrite X ; clear X.
      rewrite isrdistr_mult_plusNonnegativeRationals, islunit_oneNonnegativeRationals.
      reflexivity.
    + exact (pr2 (pr2 q)).
    + exact (pr2 (pr2 q)).
Qed.

Structures


Definition Dcuts_setwith2binop : setwith2binop.
Proof.
   Dcuts.
  split.
  - exact Dcuts_plus.
  - exact Dcuts_mult.
Defined.

Definition isabmonoidop_Dcuts_plus : isabmonoidop Dcuts_plus.
Proof.
  repeat split.
  - exact isassoc_Dcuts_plus.
  - Dcuts_zero.
    split.
    + exact islunit_Dcuts_plus_zero.
    + exact isrunit_Dcuts_plus_zero.
  - exact iscomm_Dcuts_plus.
Defined.

Definition ismonoidop_Dcuts_mult : ismonoidop Dcuts_mult.
Proof.
  split.
  - exact isassoc_Dcuts_mult.
  - Dcuts_one.
    split.
    + exact islunit_Dcuts_mult_one.
    + exact isrunit_Dcuts_mult_one.
Defined.

Definition Dcuts_commrig : commrig.
Proof.
   Dcuts_setwith2binop.
  repeat split.
  - (isabmonoidop_Dcuts_plus,,ismonoidop_Dcuts_mult).
    split.
    + exact islabsorb_Dcuts_mult_zero.
    + exact israbsorb_Dcuts_mult_zero.
  - exact isldistr_Dcuts_plus_mult.
  - exact isrdistr_Dcuts_plus_mult.
  - exact iscomm_Dcuts_mult.
Defined.

Definition Dcuts_ConstructiveCommutativeDivisionRig : ConstructiveCommutativeDivisionRig.
Proof.
   Dcuts_commrig.
   (pr2 Dcuts).
  repeat split.
  - exact islapbinop_Dcuts_plus.
  - exact israpbinop_Dcuts_plus.
  - exact islapbinop_Dcuts_mult.
  - exact israpbinop_Dcuts_mult.
  - exact Dcuts_ap_one_zero.
  - intros x Hx.
     (Dcuts_inv x Hx) ; split.
    + exact (islinv_Dcuts_inv x Hx).
    + exact (isrinv_Dcuts_inv x Hx).
Defined.

Additional usefull definitions

Dcuts_minus


Section Dcuts_minus.

  Context (X : hsubtype NonnegativeRationals).
  Context (X_bot : Dcuts_def_bot X).
  Context (X_open : Dcuts_def_open X).
  Context (X_corr : Dcuts_def_corr X).
  Context (Y : hsubtype NonnegativeRationals).
  Context (Y_bot : Dcuts_def_bot Y).
  Context (Y_open : Dcuts_def_open Y).
  Context (Y_corr : Dcuts_def_corr Y).

Definition Dcuts_minus_val : hsubtype NonnegativeRationals :=
  λ r, x, X x × y, (Y y) ⨿ (y = 0%NRat) (r + y < x)%NRat.

Lemma Dcuts_minus_bot : Dcuts_def_bot Dcuts_minus_val.
Proof.
  intros r Hr q Hle.
  revert Hr ; apply hinhfun ; intros x.
   (pr1 x) ; split.
  - exact (pr1 (pr2 x)).
  - intros y Yy.
    apply istrans_le_lt_ltNonnegativeRationals with (r + y).
    apply plusNonnegativeRationals_lecompat_r.
    exact Hle.
    now apply (pr2 (pr2 x)).
Qed.

Lemma Dcuts_minus_open : Dcuts_def_open Dcuts_minus_val.
Proof.
  intros r.
  apply hinhuniv ; intros x.
  generalize (X_open _ (pr1 (pr2 x))).
  apply hinhfun ; intros x'.
   (r + (pr1 x' - pr1 x)) ; split.
  - apply hinhpr ; (pr1 x') ; split.
    + exact (pr1 (pr2 x')).
    + intros y Yy.
      pattern (pr1 x') at 2 ;
        rewrite <- (minusNonnegativeRationals_plus_r _ _ (lt_leNonnegativeRationals _ _ (pr2 (pr2 x')))).
      rewrite (iscomm_plusNonnegativeRationals r), isassoc_plusNonnegativeRationals.
      apply plusNonnegativeRationals_ltcompat_l.
      now apply (pr2 (pr2 x)).
  - apply plusNonnegativeRationals_lt_r.
    apply ispositive_minusNonnegativeRationals.
    exact (pr2 (pr2 x')).
Qed.

Lemma Dcuts_minus_corr : Dcuts_def_corr Dcuts_minus_val.
Proof.
  assert (Y_corr' : Dcuts_def_corr (λ y, Y y (y = 0%NRat))).
  { intros c Hc.
    generalize (Y_corr c Hc) ; apply hinhfun ; apply sumofmaps ; [intros Yc | intros y ].
    - left.
      intros H ; apply Yc ; clear Yc ; revert H.
      apply hinhuniv ; apply sumofmaps ; [intros Yc | intros Hc0].
      + exact Yc.
      + rewrite Hc0 in Hc.
        now apply fromempty, (isirrefl_ltNonnegativeRationals 0%NRat).
    - right.
       (pr1 y) ; split.
      + apply hinhpr ; left.
        exact (pr1 (pr2 y)).
      + intros H ; apply (pr2 (pr2 y)) ; revert H.
        apply hinhuniv ; apply sumofmaps ; [intros H | intros Hc0].
        × exact H.
        × apply fromempty ; revert Hc0.
          apply gtNonnegativeRationals_noteq.
          now apply ispositive_plusNonnegativeRationals_r. }
  intros c Hc.
  apply ispositive_NQhalf in Hc.
  apply (λ X X0 Xerr, Dcuts_def_corr_not_empty X X0 Xerr _ Hc) in Y_corr'.
  revert Y_corr' ; apply hinhuniv ; intros y.
  generalize (pr1 (pr2 y)) ; apply hinhuniv ; intros Yy.
  assert (X0 : ¬ Y (pr1 y + c / 2%NRat)).
  { intro ; apply (pr2 (pr2 y)).
    now apply hinhpr ; left. }
  rename X0 into nYy.
  generalize (X_corr _ Hc) ; apply hinhuniv ; apply sumofmaps ; [intros Xc | intros x].

  - apply hinhpr ; left ; intro H ; apply Xc.
    revert H ; apply hinhuniv ; intros x.
    apply X_bot with (1 := pr1 (pr2 x)).
    apply istrans_leNonnegativeRationals with c.
    pattern c at 2 ; rewrite (NQhalf_double c).
    now apply plusNonnegativeRationals_le_r.
    apply lt_leNonnegativeRationals.
    pattern c at 1 ;
      rewrite <- (isrunit_zeroNonnegativeRationals c).
    apply (pr2 (pr2 x)).
    now right.
  - generalize (isdecrel_leNonnegativeRationals (pr1 y + c / 2)%NRat (pr1 x)) ; apply sumofmaps ; intro Hxy.
    + assert (HY : y', (Y y') ⨿ (y' = 0%NRat) (y' < pr1 y + c / 2)%NRat).
      { intros y' ; apply sumofmaps ; intros Yy'.
        apply notge_ltNonnegativeRationals ; intro H ; apply nYy.
        now apply Y_bot with (1 := Yy').
        rewrite Yy'.
        now apply ispositive_plusNonnegativeRationals_r. }
      apply hinhpr ; right ; (pr1 x - (pr1 y + c / 2))%NRat ; split.
      × apply hinhpr.
         (pr1 x) ; split.
        exact (pr1 (pr2 x)).
        intros y' Yy'.
        pattern (pr1 x) at 2 ;
        rewrite <- (minusNonnegativeRationals_plus_r _ _ Hxy).
        apply plusNonnegativeRationals_ltcompat_l.
        now apply HY.
      × unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros x'.
        generalize (pr2 (pr2 x') (pr1 y) Yy).
        apply_pr2 notlt_geNonnegativeRationals.
        apply istrans_leNonnegativeRationals with (pr1 x + c / 2)%NRat.
        apply lt_leNonnegativeRationals.
        apply notge_ltNonnegativeRationals ; intro H ; apply (pr2 (pr2 x)).
        now apply X_bot with (1 := pr1 (pr2 x')).
        rewrite isassoc_plusNonnegativeRationals, (iscomm_plusNonnegativeRationals _ (pr1 y)).
        pattern c at 3; rewrite (NQhalf_double c).
        rewrite <- (isassoc_plusNonnegativeRationals (pr1 y)), <- isassoc_plusNonnegativeRationals.
        rewrite minusNonnegativeRationals_plus_r.
        apply isrefl_leNonnegativeRationals.
        exact Hxy.
    + apply notge_ltNonnegativeRationals in Hxy.
      apply hinhpr ; left ; unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros x'.
      generalize (pr2 (pr2 x') _ Yy).
      apply_pr2 notlt_geNonnegativeRationals.
      induction (isdecrel_leNonnegativeRationals (pr1 y) (pr1 x')) as [Hxy' | Hxy'].
      rewrite iscomm_plusNonnegativeRationals.
      pattern c at 1; rewrite (NQhalf_double c), <- isassoc_plusNonnegativeRationals.
      apply istrans_leNonnegativeRationals with (pr1 x + c / 2)%NRat.
      apply lt_leNonnegativeRationals ; apply notge_ltNonnegativeRationals ; intro ; apply (pr2 (pr2 x)).
      now apply X_bot with (1 := pr1 (pr2 x')).
      apply plusNonnegativeRationals_lecompat_r.
      now apply lt_leNonnegativeRationals.
      apply notge_ltNonnegativeRationals in Hxy'.
      apply istrans_leNonnegativeRationals with (pr1 y).
      now apply lt_leNonnegativeRationals.
      now apply plusNonnegativeRationals_le_l.
  - now apply hinhpr ; right.
Qed.

End Dcuts_minus.

Definition Dcuts_minus (X Y : Dcuts) : Dcuts :=
  make_Dcuts (Dcuts_minus_val (pr1 X) (pr1 Y))
           (Dcuts_minus_bot (pr1 X) (pr1 Y))
           (Dcuts_minus_open (pr1 X) (is_Dcuts_open X) (pr1 Y))
           (Dcuts_minus_corr (pr1 X) (is_Dcuts_bot X) (is_Dcuts_corr X)
                              (pr1 Y) (is_Dcuts_bot Y) (is_Dcuts_corr Y)).

Lemma Dcuts_minus_correct_l:
   x y z : Dcuts, x = Dcuts_plus y z z = Dcuts_minus x y.
Proof.
  intros _ Y Z →.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - intros Zr.
    generalize (is_Dcuts_open _ _ Zr) ; apply hinhuniv ; intros q.
    generalize (pr1 (ispositive_minusNonnegativeRationals _ _) (pr2 (pr2 q))) ; intros Hq.
    generalize (is_Dcuts_corr Y _ Hq) ; apply hinhuniv ; apply sumofmaps ; [intros nYy | ].
    + apply hinhpr ; (pr1 q) ; split.
      × apply hinhpr ; left ; right.
        exact (pr1 (pr2 q)).
      × intros y ; apply sumofmaps ; [intros Yy | intros ->].
        apply minusNonnegativeRationals_ltcompat_l' with r.
        rewrite plusNonnegativeRationals_minus_l.
        now apply (Dcuts_finite Y).
        rewrite isrunit_zeroNonnegativeRationals.
        now apply_pr2 ispositive_minusNonnegativeRationals.
    + intros y.
      apply hinhpr.
       (pr1 y + pr1 q) ; split.
      apply hinhpr ; right ; (pr1 y,,pr1 q) ; simpl ; repeat split.
      × exact (pr1 (pr2 y)).
      × exact (pr1 (pr2 q)).
      × intros y' ; apply sumofmaps ; [intros Yy' | intros ->].
        apply minusNonnegativeRationals_ltcompat_l' with r.
        rewrite plusNonnegativeRationals_minus_l.
        rewrite iscomm_plusNonnegativeRationals, <- minusNonnegativeRationals_plus_exchange, iscomm_plusNonnegativeRationals.
        apply (Dcuts_finite Y).
        exact (pr2 (pr2 y)).
        exact Yy'.
        now apply lt_leNonnegativeRationals ; apply_pr2 ispositive_minusNonnegativeRationals.
        rewrite isrunit_zeroNonnegativeRationals.
        apply istrans_lt_le_ltNonnegativeRationals with (pr1 q).
        now apply_pr2 ispositive_minusNonnegativeRationals.
        now apply plusNonnegativeRationals_le_l.
  - apply hinhuniv ; intros q.
    generalize (pr1 (pr2 q)) ; apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros Yq | intros Zq ] | intros yz ].
    + apply fromempty, (isnonnegative_NonnegativeRationals' r).
      apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 q)).
      rewrite islunit_zeroNonnegativeRationals.
      apply (pr2 (pr2 q)).
      now left.
    + apply is_Dcuts_bot with (1 := Zq), lt_leNonnegativeRationals.
      pattern r at 1 ;
        rewrite <- (isrunit_zeroNonnegativeRationals r).
      apply (pr2 (pr2 q)).
      now right.
    + apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 yz))), lt_leNonnegativeRationals.
      apply_pr2 (plusNonnegativeRationals_ltcompat_l (pr1 (pr1 yz))).
      rewrite <- (pr1 (pr2 yz)), iscomm_plusNonnegativeRationals.
      apply (pr2 (pr2 q)).
      left.
      exact (pr1 (pr2 (pr2 yz))).
Qed.
Lemma Dcuts_minus_correct_r:
   x y z : Dcuts, x = Dcuts_plus y z y = Dcuts_minus x z.
Proof.
  intros x y z Hx.
  apply Dcuts_minus_correct_l.
  rewrite Hx.
  now apply iscomm_Dcuts_plus.
Qed.
Lemma Dcuts_minus_eq_zero:
   x y : Dcuts, x y Dcuts_minus x y = 0.
Proof.
  intros X Y Hxy.
  apply Dcuts_eq_is_eq ; intros r ; split.
  - apply hinhuniv ; intros x.
    apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 x)).
    rewrite islunit_zeroNonnegativeRationals.
    apply (pr2 (pr2 x)).
    left ; simple refine (Hxy _ _).
    exact (pr1 (pr2 x)).
  - intro H.
    now apply fromempty ; apply (Dcuts_zero_empty r).
Qed.
Lemma Dcuts_minus_plus_r:
   x y z : Dcuts, z y x = Dcuts_minus y z y = Dcuts_plus x z.
Proof.
  intros _ Y Z Hyz →.
  apply Dcuts_eq_is_eq ; intro r ; split.
  - intros Yr.
    generalize (is_Dcuts_open _ _ Yr) ; apply hinhuniv ; intros q.
    generalize (pr1 (ispositive_minusNonnegativeRationals _ _) (pr2 (pr2 q))) ; intros Hq.
    generalize (is_Dcuts_corr Z _ Hq).
    apply hinhuniv ; apply sumofmaps ; [intros nZ | ].
    + apply hinhpr ; left ; left.
      apply hinhpr.
       (pr1 q) ; split.
      exact (pr1 (pr2 q)).
      intros z ; apply sumofmaps ; [intros Zz | intros ->].
      × apply (minusNonnegativeRationals_ltcompat_l' _ _ r).
        rewrite plusNonnegativeRationals_minus_l.
        now apply (Dcuts_finite Z).
      × now rewrite isrunit_zeroNonnegativeRationals ;
        apply_pr2 ispositive_minusNonnegativeRationals.
    + intros z.
      induction (isdecrel_leNonnegativeRationals r (pr1 z)) as [Hzr | Hzr].
      × apply hinhpr ; left ; right.
        now apply (is_Dcuts_bot _ _ (pr1 (pr2 z))).
      × apply notge_ltNonnegativeRationals in Hzr ; apply lt_leNonnegativeRationals in Hzr.
        apply hinhpr ; right.
         (r - pr1 z ,, pr1 z) ; repeat split.
        simpl.
        now rewrite minusNonnegativeRationals_plus_r.
        apply hinhpr ; simpl.
         (pr1 q) ; split.
        exact (pr1 (pr2 q)).
        intros z' ; apply sumofmaps ; [intros Zz' | intros ->].
        apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 z)).
        rewrite isassoc_plusNonnegativeRationals, (iscomm_plusNonnegativeRationals z'), <- isassoc_plusNonnegativeRationals.
        rewrite minusNonnegativeRationals_plus_r.
        apply (minusNonnegativeRationals_ltcompat_l' _ _ r) ; rewrite plusNonnegativeRationals_minus_l.
        rewrite <- minusNonnegativeRationals_plus_exchange, iscomm_plusNonnegativeRationals.
        apply (Dcuts_finite Z).
        exact (pr2 (pr2 z)).
        exact Zz'.
        now apply lt_leNonnegativeRationals ; apply_pr2 ispositive_minusNonnegativeRationals.
        now apply Hzr.
        rewrite isrunit_zeroNonnegativeRationals.
        apply istrans_le_lt_ltNonnegativeRationals with r.
        now apply minusNonnegativeRationals_le.
        now apply_pr2 ispositive_minusNonnegativeRationals.
        exact (pr1 (pr2 z)).
  - apply hinhuniv ; apply sumofmaps ; [apply sumofmaps ; [ | intros Zr] | intros ryzz ; rewrite (pr1 (pr2 ryzz)) ].
    + apply hinhuniv ; intros y.
      apply (is_Dcuts_bot _ _ (pr1 (pr2 y))).
      apply lt_leNonnegativeRationals.
      pattern r at 1 ;
      rewrite <- (isrunit_zeroNonnegativeRationals r).
      apply (pr2 (pr2 y)).
      now right.
    + now simple refine (Hyz _ _).
    + generalize (pr1 (pr2 (pr2 ryzz))) ; apply hinhuniv ; simpl ; intros y.
      apply (is_Dcuts_bot _ _ (pr1 (pr2 y))).
      apply lt_leNonnegativeRationals, (pr2 (pr2 y)).
      left.
      exact (pr2 (pr2 (pr2 ryzz))).
Qed.

Lemma Dcuts_minus_le :
   x y, Dcuts_minus x y x.
Proof.
  intros X Y r.
  apply hinhuniv ; intros x.
  apply is_Dcuts_bot with (1 := pr1 (pr2 x)).
  apply lt_leNonnegativeRationals.
  pattern r at 1 ;
    rewrite <- (isrunit_zeroNonnegativeRationals r).
  apply (pr2 (pr2 x)).
  now right.
Qed.

Lemma ispositive_Dcuts_minus :
   x y : Dcuts, (y < x) (0 < Dcuts_minus x y).
Proof.
  intros X Y.
  split.
  - apply hinhuniv ; intros x.
    generalize (is_Dcuts_open _ _ (pr2 (pr2 x))) ; apply hinhfun ; intros x'.
     0%NRat ; split.
    + now apply (isnonnegative_NonnegativeRationals' 0%NRat).
    + apply hinhpr.
       (pr1 x') ; split.
      exact (pr1 (pr2 x')).
      intros y ; apply sumofmaps ; [intros Yy | intros ->].
      × rewrite islunit_zeroNonnegativeRationals.
        apply istrans_ltNonnegativeRationals with (pr1 x).
        apply (Dcuts_finite Y).
        exact (pr1 (pr2 x)).
        exact Yy.
        exact (pr2 (pr2 x')).
      × rewrite islunit_zeroNonnegativeRationals.
        apply istrans_le_lt_ltNonnegativeRationals with (pr1 x).
        now apply isnonnegative_NonnegativeRationals.
        exact (pr2 (pr2 x')).
  - apply hinhuniv ; intros r ; generalize (pr2 (pr2 r)).
    apply hinhfun ; intros x.
     (pr1 x) ; split.
    + intros Yx ; apply (isnonnegative_NonnegativeRationals' (pr1 r)).
      apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 x)).
      rewrite islunit_zeroNonnegativeRationals.
      now apply (pr2 (pr2 x)) ; left.
    + exact (pr1 (pr2 x)).
Qed.

Dcuts_max


Section Dcuts_max.

  Context (X : hsubtype NonnegativeRationals).
  Context (X_bot : Dcuts_def_bot X).
  Context (X_open : Dcuts_def_open