Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Spaces.No.Core.

Local Open Scope path_scope.
Local Open Scope surreal_scope.

(** * Negation of surreal numbers *)

(** Negation requires the option sorts to be symmetric. *)
Class HasNegation (S : OptionSort) 
  := symmetric_options :: forall L R, InSort S L R -> InSort S R L.

Instance hasnegation_maxsort : HasNegation MaxSort
  := fun _ _ _ => tt.

Instance hasnegation_decsort : HasNegation DecSort.
HasNegation DecSort
Proof.
HasNegation DecSort
  intros L R [? ?]; split; assumption.
Qed.

Section HasNegation.
  Universe i.
  Context {S : OptionSort@{i}} `{HasNegation S}.
  Let No := GenNo S.

  Definition negate : No -> No.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
No -> No
  Proof.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
No -> No
    simple refine (No_rec No (fun x y => y <= x) (fun x y => y < x)
                          _ _ _ _ _); intros.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
No
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
a, b: No
X: (fun x y : No => y <= x) a b
X0: (fun x y : No => y <= x) b a
a = b
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'),
(fun x y : No => y < x) (fyL l) (fyR r)
p: forall l : L, xL l < {{ yL | yR//ycut }}
dp: forall l : L,
(fun x y : No => y < x) (fxL l)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l0 : L) 
              (r : R), xL l0 < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l0 : L) 
               (r : R),
               (fun x y : No => y < x) 
                 (fxL l0) 
                 (fxR r)) => 
    ?Goal) L' R' s' yL yR ycut fyL fyR fycut)
q: forall r : R', {{ xL | xR//xcut }} < yR r
dq: forall r : R',
(fun x y : No => y < x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) 
              (r0 : R), xL l < xR r0)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r0 : R),
               (fun x y : No => y < x) 
                 (fxL l) 
                 (fxR r0)) => 
    ?Goal) L R s xL xR xcut fxL fxR fxcut)
  (fyR r)
(fun x y : No => y <= x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    => ?Goal) L R s xL xR xcut fxL fxR fxcut)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    => ?Goal) L' R' s' yL yR ycut fyL fyR fycut)
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'),
(fun x y : No => y < x) (fyL l) (fyR r)
l: L'
p: {{ xL | xR//xcut }} <= yL l
dp: (fun x y : No => y <= x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) 
                 (fxL l) 
                 (fxR r)) => 
    ?Goal) L R s xL xR xcut fxL fxR fxcut)
  (fyL l)
(fun x y : No => y < x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    => ?Goal) L R s xL xR xcut fxL fxR fxcut)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    => ?Goal) L' R' s' yL yR ycut fyL fyR fycut)
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'),
(fun x y : No => y < x) (fyL l) (fyR r)
r: R
p: xR r <= {{ yL | yR//ycut }}
dp: (fun x y : No => y <= x) 
  (fxR r)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) 
                 (fxL l) 
                 (fxR r)) => 
    ?Goal) L' R' s' yL yR ycut fyL fyR fycut)
(fun x y : No => y < x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    => ?Goal) L R s xL xR xcut fxL fxR fxcut)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (xcut : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    => ?Goal) L' R' s' yL yR ycut fyL fyR fycut)
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
No exact {{ fxR | fxL // fun r l => fxcut l r }}.
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
a, b: No
X: (fun x y : No => y <= x) a b
X0: (fun x y : No => y <= x) b a
a = b apply path_No; assumption.
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'),
(fun x y : No => y < x) (fyL l) (fyR r)
p: forall l : L, xL l < {{ yL | yR//ycut }}
dp: forall l : L,
(fun x y : No => y < x) (fxL l)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (_ : forall (l0 : L) (r : R), xL l0 < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l0 : L) 
               (r : R),
               (fun x y : No => y < x) 
                 (fxL l0) 
                 (fxR r)) =>
    {{ fxR | fxL//fun (r : R) (l0 : L) =>
                  fxcut l0 r }}) L' R' s' yL yR
     ycut fyL fyR fycut)
q: forall r : R', {{ xL | xR//xcut }} < yR r
dq: forall r : R',
(fun x y : No => y < x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (_ : forall (l : L) (r0 : R), xL l < xR r0)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r0 : R),
               (fun x y : No => y < x) 
                 (fxL l) 
                 (fxR r0)) =>
    {{ fxR | fxL//fun (r0 : R) (l : L) =>
                  fxcut l r0 }}) L R s xL xR xcut
     fxL fxR fxcut) (fyR r)
(fun x y : No => y <= x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    =>
    {{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }})
     L R s xL xR xcut fxL fxR fxcut)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    =>
    {{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }})
     L' R' s' yL yR ycut fyL fyR fycut) cbn in *.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R), fxR r < fxL l
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'), fyR r < fyL l
p: forall l : L, xL l < {{ yL | yR//ycut }}
dp: forall l : L,
{{ fyR | fyL//fun (r : R') (l0 : L') =>
              fycut l0 r }} < 
fxL l
q: forall r : R', {{ xL | xR//xcut }} < yR r
dq: forall r : R',
fyR r <
{{ fxR | fxL//fun (r0 : R) (l : L) => fxcut l r0 }}
{{ fyR | fyL//fun (r : R') (l : L') => fycut l r }} <=
{{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }} apply le_lr; intros; [ apply dq | apply dp ].
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'),
(fun x y : No => y < x) (fyL l) (fyR r)
l: L'
p: {{ xL | xR//xcut }} <= yL l
dp: (fun x y : No => y <= x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) 
                 (fxL l) 
                 (fxR r)) =>
    {{ fxR | fxL//fun (r : R) (l : L) =>
                  fxcut l r }}) L R s xL xR xcut
     fxL fxR fxcut) (fyL l)
(fun x y : No => y < x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    =>
    {{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }})
     L R s xL xR xcut fxL fxR fxcut)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    =>
    {{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }})
     L' R' s' yL yR ycut fyL fyR fycut) cbn in *.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R), fxR r < fxL l
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'), fyR r < fyL l
l: L'
p: {{ xL | xR//xcut }} <= yL l
dp: fyL l <=
{{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }}
{{ fyR | fyL//fun (r : R') (l : L') => fycut l r }} <
{{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }} apply lt_r with l; intros; assumption.
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R),
(fun x y : No => y < x) (fxL l) (fxR r)
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'),
(fun x y : No => y < x) (fyL l) (fyR r)
r: R
p: xR r <= {{ yL | yR//ycut }}
dp: (fun x y : No => y <= x) 
  (fxR r)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) 
      (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) 
               (r : R),
               (fun x y : No => y < x) 
                 (fxL l) 
                 (fxR r)) =>
    {{ fxR | fxL//fun (r : R) (l : L) =>
                  fxcut l r }}) L' R' s' yL yR
     ycut fyL fyR fycut)
(fun x y : No => y < x)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    =>
    {{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }})
     L R s xL xR xcut fxL fxR fxcut)
  ((fun (L R : Type) (s : InSort S L R)
      (xL : L -> GenNo S) (xR : R -> GenNo S)
      (_ : forall (l : L) (r : R), xL l < xR r)
      (fxL : L -> No) (fxR : R -> No)
      (fxcut : forall (l : L) (r : R),
               (fun x y : No => y < x) (fxL l) (fxR r))
    =>
    {{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }})
     L' R' s' yL yR ycut fyL fyR fycut) cbn in *.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
s: InSort S L R
xL: L -> GenNo S
xR: R -> GenNo S
xcut: forall (l : L) (r : R), xL l < xR r
fxL: L -> No
fxR: R -> No
fxcut: forall (l : L) (r : R), fxR r < fxL l
L', R': Type
s': InSort S L' R'
yL: L' -> GenNo S
yR: R' -> GenNo S
ycut: forall (l : L') (r : R'), yL l < yR r
fyL: L' -> No
fyR: R' -> No
fycut: forall (l : L') (r : R'), fyR r < fyL l
r: R
p: xR r <= {{ yL | yR//ycut }}
dp: {{ fyR | fyL//fun (r : R') (l : L') => fycut l r }} <=
fxR r
{{ fyR | fyL//fun (r : R') (l : L') => fycut l r }} <
{{ fxR | fxL//fun (r : R) (l : L) => fxcut l r }} apply lt_l with r; intros; assumption.
  Defined.

  (** More useful is the following rewriting lemma. *)
  Definition negate_cut
             {L R : Type@{i} } {Sx : InSort S L R}
             (xL : L -> No) (xR : R -> No)
             (xcut : forall (l : L) (r : R), xL l < xR r)
    : { nxcut : forall r l, negate (xR r) < negate (xL l) &
        negate {{ xL | xR // xcut }} =
        {{ (fun r => negate (xR r)) | (fun l => negate (xL l)) // nxcut }} }.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
Sx: InSort S L R
xL: L -> No
xR: R -> No
xcut: forall (l : L) (r : R), xL l < xR r
{nxcut
: forall (r : R) (l : L),
  negate (xR r) < negate (xL l) &
negate {{ xL | xR//xcut }} =
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }}}
  Proof.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
Sx: InSort S L R
xL: L -> No
xR: R -> No
xcut: forall (l : L) (r : R), xL l < xR r
{nxcut
: forall (r : R) (l : L),
  negate (xR r) < negate (xL l) &
negate {{ xL | xR//xcut }} =
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }}}
    eexists.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
Sx: InSort S L R
xL: L -> No
xR: R -> No
xcut: forall (l : L) (r : R), xL l < xR r
negate {{ xL | xR//xcut }} =
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//?nxcut }}
    unfold negate at 1; rewrite No_rec_cut.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
L, R: Type
Sx: InSort S L R
xL: L -> No
xR: R -> No
xcut: forall (l : L) (r : R), xL l < xR r
{{ fun r : R =>
   No_rec No (fun x y : No => y <= x)
     (fun x y : No => y < x)
     (fun (L R : Type) (s : InSort S L R)
        (xL : L -> GenNo S) (xR : R -> GenNo S)
        (_ : forall (l : L) (r0 : R), xL l < xR r0)
        (fxL : L -> No) (fxR : R -> No)
        (fxcut : forall (l : L) (r0 : R),
                 fxR r0 < fxL l) =>
      {{ fxR | fxL//fun (r0 : R) (l : L) => fxcut l r0 }})
     (fun (a b : No) (H : b <= a) (H0 : a <= b) =>
      path_No a b H0 H)
     (fun (L R : Type) (s : InSort S L R)
        (xL : L -> GenNo S) (xR : R -> GenNo S)
        (xcut : forall (l : L) (r0 : R), xL l < xR r0)
        (fxL : L -> No) (fxR : R -> No)
        (fxcut : forall (l : L) (r0 : R),
                 fxR r0 < fxL l) (L' R' : Type)
        (s' : InSort S L' R') (yL : L' -> GenNo S)
        (yR : R' -> GenNo S)
        (ycut : forall (l : L') (r0 : R'),
                yL l < yR r0) (fyL : L' -> No)
        (fyR : R' -> No)
        (fycut : forall (l : L') (r0 : R'),
                 fyR r0 < fyL l)
        (_ : forall l : L, xL l < {{ yL | yR//ycut }})
        (dp : forall l : L,
              {{ fyR | fyL//fun (r0 : R') (l0 : L') =>
                            fycut l0 r0 }} < fxL l)
        (_ : forall r0 : R',
             {{ xL | xR//xcut }} < yR r0)
        (dq : forall r0 : R',
              fyR r0 <
              {{ fxR | fxL//fun (r1 : R) (l : L) =>
                            fxcut l r1 }}) =>
      le_lr fyR fyL
        (fun (r0 : R') (l : L') => fycut l r0) fxR fxL
        (fun (r0 : R) (l : L) => fxcut l r0)
        (fun l : R' => dq l) (fun r0 : L => dp r0))
     (fun (L R : Type) (s : InSort S L R)
        (xL : L -> GenNo S) (xR : R -> GenNo S)
        (xcut : forall (l : L) (r0 : R), xL l < xR r0)
        (fxL : L -> No) (fxR : R -> No)
        (fxcut : forall (l : L) (r0 : R),
                 fxR r0 < fxL l) (L' R' : Type)
        (s' : InSort S L' R') (yL : L' -> GenNo S)
        (yR : R' -> GenNo S)
        (_ : forall (l : L') (r0 : R'), yL l < yR r0)
        (fyL : L' -> No) (fyR : R' -> No)
        (fycut : forall (l : L') (r0 : R'),
                 fyR r0 < fyL l) (l : L')
        (_ : {{ xL | xR//xcut }} <= yL l)
        (dp : fyL l <=
              {{ fxR | fxL//fun (r0 : R) (l0 : L) =>
                            fxcut l0 r0 }}) =>
      lt_r fyR fyL
        (fun (r0 : R') (l0 : L') => fycut l0 r0) fxR
        fxL (fun (r0 : R) (l0 : L) => fxcut l0 r0) l
        dp)
     (fun (L R : Type) (s : InSort S L R)
        (xL : L -> GenNo S) (xR : R -> GenNo S)
        (_ : forall (l : L) (r0 : R), xL l < xR r0)
        (fxL : L -> No) (fxR : R -> No)
        (fxcut : forall (l : L) (r0 : R),
                 fxR r0 < fxL l) (L' R' : Type)
        (s' : InSort S L' R') (yL : L' -> GenNo S)
        (yR : R' -> GenNo S)
        (ycut : forall (l : L') (r0 : R'),
                yL l < yR r0) (fyL : L' -> No)
        (fyR : R' -> No)
        (fycut : forall (l : L') (r0 : R'),
                 fyR r0 < fyL l) (r0 : R)
        (_ : xR r0 <= {{ yL | yR//ycut }})
        (dp : {{ fyR | fyL//fun (r1 : R') (l : L') =>
                            fycut l r1 }} <= fxR r0)
      =>
      lt_l fyR fyL
        (fun (r1 : R') (l : L') => fycut l r1) fxR fxL
        (fun (r1 : R) (l : L) => fxcut l r1) r0 dp)
     (xR r) | (fun l : L =>
               No_rec No (fun x y : No => y <= x)
                 (fun x y : No => y < x)
                 (fun (L R : Type) (s : InSort S L R)
                    (xL : L -> GenNo S)
                    (xR : R -> GenNo S)
                    (_ : forall (l0 : L) (r : R),
                         xL l0 < xR r) (fxL : L -> No)
                    (fxR : R -> No)
                    (fxcut : forall (l0 : L) (r : R),
                             fxR r < fxL l0) =>
                  {{ fxR | fxL//fun (r : R) (l0 : L)
                                => fxcut l0 r }})
                 (fun (a b : No) (H : b <= a)
                    (H0 : a <= b) => path_No a b H0 H)
                 (fun (L R : Type) (s : InSort S L R)
                    (xL : L -> GenNo S)
                    (xR : R -> GenNo S)
                    (xcut : forall (l0 : L) (r : R),
                            xL l0 < xR r)
                    (fxL : L -> No) (fxR : R -> No)
                    (fxcut : forall (l0 : L) (r : R),
                             fxR r < fxL l0)
                    (L' R' : Type)
                    (s' : InSort S L' R')
                    (yL : L' -> GenNo S)
                    (yR : R' -> GenNo S)
                    (ycut : forall (l0 : L') (r : R'),
                            yL l0 < yR r)
                    (fyL : L' -> No) (fyR : R' -> No)
                    (fycut : forall (l0 : L')
                             (r : R'), fyR r < fyL l0)
                    (_ : forall l0 : L,
                         xL l0 < {{ yL | yR//ycut }})
                    (dp : forall l0 : L,
                          {{ fyR | fyL//fun (r : R')
                                          (l1 : L') =>
                                        fycut l1 r }} <
                          fxL l0)
                    (_ : forall r : R',
                         {{ xL | xR//xcut }} < yR r)
                    (dq : forall r : R',
                          fyR r <
                          {{ fxR | fxL//fun (r0 : R)
                                          (l0 : L) =>
                                        fxcut l0 r0 }})
                  =>
                  le_lr fyR fyL
                    (fun (r : R') (l0 : L') =>
                     fycut l0 r) fxR fxL
                    (fun (r : R) (l0 : L) =>
                     fxcut l0 r)
                    (fun l0 : R' => dq l0)
                    (fun r : L => dp r))
                 (fun (L R : Type) (s : InSort S L R)
                    (xL : L -> GenNo S)
                    (xR : R -> GenNo S)
                    (xcut : forall (l0 : L) (r : R),
                            xL l0 < xR r)
                    (fxL : L -> No) (fxR : R -> No)
                    (fxcut : forall (l0 : L) (r : R),
                             fxR r < fxL l0)
                    (L' R' : Type)
                    (s' : InSort S L' R')
                    (yL : L' -> GenNo S)
                    (yR : R' -> GenNo S)
                    (_ : forall (l0 : L') (r : R'),
                         yL l0 < yR r)
                    (fyL : L' -> No) (fyR : R' -> No)
                    (fycut : forall (l0 : L')
                             (r : R'), fyR r < fyL l0)
                    (l0 : L')
                    (_ : {{ xL | xR//xcut }} <= yL l0)
                    (dp : fyL l0 <=
                          {{ fxR | fxL//fun (r : R)
                                          (l1 : L) =>
                                        fxcut l1 r }})
                  =>
                  lt_r fyR fyL
                    (fun (r : R') (l1 : L') =>
                     fycut l1 r) fxR fxL
                    (fun (r : R) (l1 : L) =>
                     fxcut l1 r) l0 dp)
                 (fun (L R : Type) (s : InSort S L R)
                    (xL : L -> GenNo S)
                    (xR : R -> GenNo S)
                    (_ : forall (l0 : L) (r : R),
                         xL l0 < xR r) (fxL : L -> No)
                    (fxR : R -> No)
                    (fxcut : forall (l0 : L) (r : R),
                             fxR r < fxL l0)
                    (L' R' : Type)
                    (s' : InSort S L' R')
                    (yL : L' -> GenNo S)
                    (yR : R' -> GenNo S)
                    (ycut : forall (l0 : L') (r : R'),
                            yL l0 < yR r)
                    (fyL : L' -> No) (fyR : R' -> No)
                    (fycut : forall (l0 : L')
                             (r : R'), fyR r < fyL l0)
                    (r : R)
                    (_ : xR r <= {{ yL | yR//ycut }})
                    (dp : {{ fyR | fyL//fun (r0 : R')
                                          (l0 : L') =>
                                        fycut l0 r0 }} <=
                          fxR r) =>
                  lt_l fyR fyL
                    (fun (r0 : R') (l0 : L') =>
                     fycut l0 r0) fxR fxL
                    (fun (r0 : R) (l0 : L) =>
                     fxcut l0 r0) r dp) (xL l))//fun
                                                 (r : R)
                                                 (l : L)
                                                 =>
                                                 No_rec_lt
                                                 No
                                                 (fun
                                                 x
                                                 y : No
                                                 =>
                                                 y <=
                                                 x)
                                                 (fun
                                                 x
                                                 y : No
                                                 =>
                                                 y < x)
                                                 (fun
                                                 (L
                                                 R : Type)
                                                 (s : 
                                                 InSort
                                                 S L R)
                                                 (xL : 
                                                 L ->
                                                 GenNo
                                                 S)
                                                 (xR : 
                                                 R ->
                                                 GenNo
                                                 S)
                                                 (_ : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 xL l0 <
                                                 xR r0)
                                                 (fxL : 
                                                 L ->
                                                 No)
                                                 (fxR : 
                                                 R ->
                                                 No)
                                                 (fxcut : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 fxR
                                                 r0 <
                                                 fxL
                                                 l0)
                                                 =>
                                                 {{ fxR | fxL//
                                                 fun
                                                 (r0 : R)
                                                 (l0 : L)
                                                 =>
                                                 fxcut
                                                 l0 r0 }})
                                                 (fun
                                                 (a
                                                 b : No)
                                                 (H : 
                                                 b <=
                                                 a)
                                                 (H0 : 
                                                 a <=
                                                 b) =>
                                                 path_No
                                                 a b
                                                 H0 H)
                                                 (fun
                                                 (L
                                                 R : Type)
                                                 (s : 
                                                 InSort
                                                 S L R)
                                                 (xL : 
                                                 L ->
                                                 GenNo
                                                 S)
                                                 (xR : 
                                                 R ->
                                                 GenNo
                                                 S)
                                                 (xcut : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 xL l0 <
                                                 xR r0)
                                                 (fxL : 
                                                 L ->
                                                 No)
                                                 (fxR : 
                                                 R ->
                                                 No)
                                                 (fxcut : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 fxR
                                                 r0 <
                                                 fxL
                                                 l0)
                                                 (L'
                                                 R' : Type)
                                                 (s' : 
                                                 InSort
                                                 S L'
                                                 R')
                                                 (yL : 
                                                 L' ->
                                                 GenNo
                                                 S)
                                                 (yR : 
                                                 R' ->
                                                 GenNo
                                                 S)
                                                 (ycut : 
                                                 forall
                                                 (l0 : L')
                                                 (r0 : R'),
                                                 yL l0 <
                                                 yR r0)
                                                 (fyL : 
                                                 L' ->
                                                 No)
                                                 (fyR : 
                                                 R' ->
                                                 No)
                                                 (fycut : 
                                                 forall
                                                 (l0 : L')
                                                 (r0 : R'),
                                                 fyR
                                                 r0 <
                                                 fyL
                                                 l0)
                                                 (_ : 
                                                 forall
                                                 l0 : L,
                                                 xL l0 <
                                                 {{ yL | yR//ycut }})
                                                 (dp : 
                                                 forall
                                                 l0 : L,
                                                 {{ fyR | fyL//
                                                 fun
                                                 (r0 : R')
                                                 (l1 : L')
                                                 =>
                                                 fycut
                                                 l1 r0 }} <
                                                 fxL
                                                 l0)
                                                 (_ : 
                                                 forall
                                                 r0 : R',
                                                 {{ xL | xR//xcut }} <
                                                 yR r0)
                                                 (dq : 
                                                 forall
                                                 r0 : R',
                                                 fyR
                                                 r0 <
                                                 {{ fxR | fxL//
                                                 fun
                                                 (r1 : R)
                                                 (l0 : L)
                                                 =>
                                                 fxcut
                                                 l0 r1 }})
                                                 =>
                                                 le_lr
                                                 fyR
                                                 fyL
                                                 (fun
                                                 (r0 : R')
                                                 (l0 : L')
                                                 =>
                                                 fycut
                                                 l0 r0)
                                                 fxR
                                                 fxL
                                                 (fun
                                                 (r0 : R)
                                                 (l0 : L)
                                                 =>
                                                 fxcut
                                                 l0 r0)
                                                 (fun
                                                 l0 : R'
                                                 =>
                                                 dq l0)
                                                 (fun
                                                 r0 : L
                                                 =>
                                                 dp r0))
                                                 (fun
                                                 (L
                                                 R : Type)
                                                 (s : 
                                                 InSort
                                                 S L R)
                                                 (xL : 
                                                 L ->
                                                 GenNo
                                                 S)
                                                 (xR : 
                                                 R ->
                                                 GenNo
                                                 S)
                                                 (xcut : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 xL l0 <
                                                 xR r0)
                                                 (fxL : 
                                                 L ->
                                                 No)
                                                 (fxR : 
                                                 R ->
                                                 No)
                                                 (fxcut : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 fxR
                                                 r0 <
                                                 fxL
                                                 l0)
                                                 (L'
                                                 R' : Type)
                                                 (s' : 
                                                 InSort
                                                 S L'
                                                 R')
                                                 (yL : 
                                                 L' ->
                                                 GenNo
                                                 S)
                                                 (yR : 
                                                 R' ->
                                                 GenNo
                                                 S)
                                                 (_ : 
                                                 forall
                                                 (l0 : L')
                                                 (r0 : R'),
                                                 yL l0 <
                                                 yR r0)
                                                 (fyL : 
                                                 L' ->
                                                 No)
                                                 (fyR : 
                                                 R' ->
                                                 No)
                                                 (fycut : 
                                                 forall
                                                 (l0 : L')
                                                 (r0 : R'),
                                                 fyR
                                                 r0 <
                                                 fyL
                                                 l0)
                                                 (l0 : L')
                                                 (_ : 
                                                 {{ xL | xR//xcut }} <=
                                                 yL l0)
                                                 (dp : 
                                                 fyL
                                                 l0 <=
                                                 {{ fxR | fxL//
                                                 fun
                                                 (r0 : R)
                                                 (l1 : L)
                                                 =>
                                                 fxcut
                                                 l1 r0 }})
                                                 =>
                                                 lt_r
                                                 fyR
                                                 fyL
                                                 (fun
                                                 (r0 : R')
                                                 (l1 : L')
                                                 =>
                                                 fycut
                                                 l1 r0)
                                                 fxR
                                                 fxL
                                                 (fun
                                                 (r0 : R)
                                                 (l1 : L)
                                                 =>
                                                 fxcut
                                                 l1 r0)
                                                 l0 dp)
                                                 (fun
                                                 (L
                                                 R : Type)
                                                 (s : 
                                                 InSort
                                                 S L R)
                                                 (xL : 
                                                 L ->
                                                 GenNo
                                                 S)
                                                 (xR : 
                                                 R ->
                                                 GenNo
                                                 S)
                                                 (_ : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 xL l0 <
                                                 xR r0)
                                                 (fxL : 
                                                 L ->
                                                 No)
                                                 (fxR : 
                                                 R ->
                                                 No)
                                                 (fxcut : 
                                                 forall
                                                 (l0 : L)
                                                 (r0 : R),
                                                 fxR
                                                 r0 <
                                                 fxL
                                                 l0)
                                                 (L'
                                                 R' : Type)
                                                 (s' : 
                                                 InSort
                                                 S L'
                                                 R')
                                                 (yL : 
                                                 L' ->
                                                 GenNo
                                                 S)
                                                 (yR : 
                                                 R' ->
                                                 GenNo
                                                 S)
                                                 (ycut : 
                                                 forall
                                                 (l0 : L')
                                                 (r0 : R'),
                                                 yL l0 <
                                                 yR r0)
                                                 (fyL : 
                                                 L' ->
                                                 No)
                                                 (fyR : 
                                                 R' ->
                                                 No)
                                                 (fycut : 
                                                 forall
                                                 (l0 : L')
                                                 (r0 : R'),
                                                 fyR
                                                 r0 <
                                                 fyL
                                                 l0)
                                                 (r0 : R)
                                                 (_ : 
                                                 xR r0 <=
                                                 {{ yL | yR//ycut }})
                                                 (dp : 
                                                 {{ fyR | fyL//
                                                 fun
                                                 (r1 : R')
                                                 (l0 : L')
                                                 =>
                                                 fycut
                                                 l0 r1 }} <=
                                                 fxR
                                                 r0)
                                                 =>
                                                 lt_l
                                                 fyR
                                                 fyL
                                                 (fun
                                                 (r1 : R')
                                                 (l0 : L')
                                                 =>
                                                 fycut
                                                 l0 r1)
                                                 fxR
                                                 fxL
                                                 (fun
                                                 (r1 : R)
                                                 (l0 : L)
                                                 =>
                                                 fxcut
                                                 l0 r1)
                                                 r0 dp)
                                                 (xL l)
                                                 (xR r)
                                                 (xcut
                                                 l r) }} =
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//?nxcut }}
    reflexivity.
  Defined.

  (** The following proof verifies that [No_rec] applied to a cut reduces definitionally to a cut with the expected options (although it does produce quite a large term). *)
  Context `{InSort S Empty Empty} `{InSort S Unit Empty}.
  Goal negate one = minusone.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
negate one = minusone
  Proof.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
negate one = minusone
    unfold one; rewrite (negate_cut _ _ _).2.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 _ : Unit
                                                 =>
                                                 negate
                                                 zero)//
(negate_cut (fun _ : Unit => zero) Empty.Empty_rec
   rempty_cut).1 }} = minusone
    apply path_No; apply le_lr; intros.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
l: Empty
negate (Empty.Empty_rec l) <
{{ Empty.Empty_rec | (fun _ : Unit => zero)//lempty_cut }}
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 _ : Unit
                                                 =>
                                                 negate
                                                 zero)//
(negate_cut (fun _ : Unit => zero) Empty.Empty_rec
   rempty_cut).1 }} < zero
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
l: Empty
Empty.Empty_rec l <
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 _ : Unit
                                                 =>
                                                 negate
                                                 zero)//
(negate_cut (fun _ : Unit => zero) Empty.Empty_rec
   rempty_cut).1 }}
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
{{ Empty.Empty_rec | (fun _ : Unit => zero)//lempty_cut }} <
negate zero
    (** Since [le_lr] only proves inequality of cuts, this would not work if [negate] didn't compute to a cut when applied to a cut. *)
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
l: Empty
negate (Empty.Empty_rec l) <
{{ Empty.Empty_rec | (fun _ : Unit => zero)//lempty_cut }} elim l.
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 _ : Unit
                                                 =>
                                                 negate
                                                 zero)//
(negate_cut (fun _ : Unit => zero) Empty.Empty_rec
   rempty_cut).1 }} < zero apply lt_r with r.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
negate zero <=
{{ Empty.Empty_rec | Empty.Empty_rec//lempty_cut }}
      unfold zero; rewrite (negate_cut _ _ _).2.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 l : Empty
                                                 =>
                                                 negate
                                                 (Empty.Empty_rec
                                                 l))//
(negate_cut Empty.Empty_rec Empty.Empty_rec lempty_cut).1 }} <=
{{ Empty.Empty_rec | Empty.Empty_rec//lempty_cut }}
      apply le_lr; apply Empty_ind.
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
l: Empty
Empty.Empty_rec l <
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 _ : Unit
                                                 =>
                                                 negate
                                                 zero)//
(negate_cut (fun _ : Unit => zero) Empty.Empty_rec
   rempty_cut).1 }} elim l.
    -
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
{{ Empty.Empty_rec | (fun _ : Unit => zero)//lempty_cut }} <
negate zero unfold zero; rewrite (negate_cut _ _ _).2.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
{{ Empty.Empty_rec | (fun _ : Unit =>
                      {{ Empty.Empty_rec | Empty.Empty_rec//lempty_cut }})//lempty_cut }} <
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 l : Empty
                                                 =>
                                                 negate
                                                 (Empty.Empty_rec
                                                 l))//
(negate_cut Empty.Empty_rec Empty.Empty_rec lempty_cut).1 }}
      apply lt_r with r.
S: OptionSort
H: HasNegation S
No:= GenNo S: Type
H0: InSort S Empty Empty
H1: InSort S Unit Empty
r: Unit
{{ Empty.Empty_rec | Empty.Empty_rec//lempty_cut }} <=
{{ fun r : Empty => negate (Empty.Empty_rec r) | (fun
                                                 l : Empty
                                                 =>
                                                 negate
                                                 (Empty.Empty_rec
                                                 l))//
(negate_cut Empty.Empty_rec Empty.Empty_rec lempty_cut).1 }}
      apply le_lr; apply Empty_ind.
  Qed.

End HasNegation.