(* -*- mode: coq; mode: visual-line -*- *)
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.
Global Existing Instance symmetric_options.

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

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