# 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.

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.

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.

### 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