Require Import HoTT.Basics.Require Import HoTT.Basics.
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 (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     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 (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l : L0) (r0 : R0), xL0 l < xR0 r0) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     L R s xL xR xcut fxL fxR fxcut)
  (fyR r)
(fun x y : No => y <= x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (xcut0 : forall (l : L0) (r : R0), xL0 l < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     L R s xL xR xcut fxL fxR fxcut)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (xcut0 : forall (l : L0) (r : R0), xL0 l < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     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 (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)
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'), (fun x y : No => y < x) (fyL l0) (fyR r)
l: L'
p: {{ xL | xR//xcut }} <= yL l
dp: (fun x y : No => y <= x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     L R s xL xR xcut fxL fxR fxcut)
  (fyL l)
(fun x y : No => y < x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     L R s xL xR xcut fxL fxR fxcut)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     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) (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)
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'), (fun x y : No => y < x) (fyL l) (fyR r0)
r: R
p: xR r <= {{ yL | yR//ycut }}
dp: (fun x y : No => y <= x) (fxR r)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l : L0) (r0 : R0), xL0 l < xR0 r0) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     L' R' s' yL yR ycut fyL fyR fycut)
(fun x y : No => y < x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l : L0) (r0 : R0), xL0 l < xR0 r0) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     L R s xL xR xcut fxL fxR fxcut)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S)
      (xcut0 : forall (l : L0) (r0 : R0), xL0 l < xR0 r0) 
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    ?Goal@{L:=L0; R:=R0; s:=s0; xL:=xL0; xR:=xR0; xcut:=xcut0; fxL:=fxL0;
           fxR:=fxR0; fxcut:=fxcut0})
     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 (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    {{ fxR0 | fxL0//fun (r : R0) (l0 : L0) => fxcut0 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 (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r0 : R0), xL0 l < xR0 r0)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    {{ fxR0 | fxL0//fun (r0 : R0) (l : L0) => fxcut0 l r0 }}) L R s xL xR
     xcut fxL fxR fxcut)
  (fyR r)
(fun x y : No => y <= x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r : R0), xL0 l < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r)) =>
    {{ fxR0 | fxL0//fun (r : R0) (l : L0) => fxcut0 l r }}) L R s xL xR xcut
     fxL fxR fxcut)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r : R0), xL0 l < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r)) =>
    {{ fxR0 | fxL0//fun (r : R0) (l : L0) => fxcut0 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 (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)
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'), (fun x y : No => y < x) (fyL l0) (fyR r)
l: L'
p: {{ xL | xR//xcut }} <= yL l
dp: (fun x y : No => y <= x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    {{ fxR0 | fxL0//fun (r : R0) (l0 : L0) => fxcut0 l0 r }}) L R s xL xR
     xcut fxL fxR fxcut)
  (fyL l)
(fun x y : No => y < x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    {{ fxR0 | fxL0//fun (r : R0) (l0 : L0) => fxcut0 l0 r }}) L R s xL xR
     xcut fxL fxR fxcut)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l0 : L0) (r : R0),
                (fun x y : No => y < x) (fxL0 l0) (fxR0 r)) =>
    {{ fxR0 | fxL0//fun (r : R0) (l0 : L0) => fxcut0 l0 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 (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
l: L'
p: {{ xL | xR//xcut }} <= yL l
dp: fyL l <= {{ fxR | fxL//fun (r : R) (l0 : L) => fxcut l0 r }}
{{ fyR | fyL//fun (r : R') (l0 : L') => fycut l0 r }} <
{{ fxR | fxL//fun (r : R) (l0 : L) => fxcut l0 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) (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)
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'), (fun x y : No => y < x) (fyL l) (fyR r0)
r: R
p: xR r <= {{ yL | yR//ycut }}
dp: (fun x y : No => y <= x) (fxR r)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r0 : R0), xL0 l < xR0 r0)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    {{ fxR0 | fxL0//fun (r0 : R0) (l : L0) => fxcut0 l r0 }}) L' R' s' yL yR
     ycut fyL fyR fycut)
(fun x y : No => y < x)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r0 : R0), xL0 l < xR0 r0)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    {{ fxR0 | fxL0//fun (r0 : R0) (l : L0) => fxcut0 l r0 }}) L R s xL xR
     xcut fxL fxR fxcut)
  ((fun (L0 R0 : Type) (s0 : InSort S L0 R0) (xL0 : L0 -> GenNo S)
      (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r0 : R0), xL0 l < xR0 r0)
      (fxL0 : L0 -> No) (fxR0 : R0 -> No)
      (fxcut0 : forall (l : L0) (r0 : R0),
                (fun x y : No => y < x) (fxL0 l) (fxR0 r0)) =>
    {{ fxR0 | fxL0//fun (r0 : R0) (l : L0) => fxcut0 l r0 }}) 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) (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
r: R
p: xR r <= {{ yL | yR//ycut }}
dp: {{ fyR | fyL//fun (r0 : R') (l : L') => fycut l r0 }} <= fxR r
{{ fyR | fyL//fun (r0 : R') (l : L') => fycut l r0 }} <
{{ fxR | fxL//fun (r0 : R) (l : L) => fxcut l r0 }} 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 (L0 R0 : Type) (s : InSort S L0 R0) (xL0 : L0 -> GenNo S)
        (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r0 : R0), xL0 l < xR0 r0)
        (fxL : L0 -> No) (fxR : R0 -> No)
        (fxcut : forall (l : L0) (r0 : R0), fxR r0 < fxL l) =>
      {{ fxR | fxL//fun (r0 : R0) (l : L0) => fxcut l r0 }})
     (fun (a b : No) (H0 : b <= a) (H1 : a <= b) => path_No a b H1 H0)
     (fun (L0 R0 : Type) (s : InSort S L0 R0) (xL0 : L0 -> GenNo S)
        (xR0 : R0 -> GenNo S)
        (xcut0 : forall (l : L0) (r0 : R0), xL0 l < xR0 r0) 
        (fxL : L0 -> No) (fxR : R0 -> No)
        (fxcut : forall (l : L0) (r0 : R0), 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 : L0, xL0 l < {{ yL | yR//ycut }})
        (dp : forall l : L0,
              {{ fyR | fyL//fun (r0 : R') (l0 : L') => fycut l0 r0 }} < fxL l)
        (_ : forall r0 : R', {{ xL0 | xR0//xcut0 }} < yR r0)
        (dq : forall r0 : R',
              fyR r0 < {{ fxR | fxL//fun (r1 : R0) (l : L0) => fxcut l r1 }}) =>
      le_lr fyR fyL (fun (r0 : R') (l : L') => fycut l r0) fxR fxL
        (fun (r0 : R0) (l : L0) => fxcut l r0) (fun l : R' => dq l)
        (fun r0 : L0 => dp r0))
     (fun (L0 R0 : Type) (s : InSort S L0 R0) (xL0 : L0 -> GenNo S)
        (xR0 : R0 -> GenNo S)
        (xcut0 : forall (l : L0) (r0 : R0), xL0 l < xR0 r0) 
        (fxL : L0 -> No) (fxR : R0 -> No)
        (fxcut : forall (l : L0) (r0 : R0), 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') (_ : {{ xL0 | xR0//xcut0 }} <= yL l)
        (dp : fyL l <=
              {{ fxR | fxL//fun (r0 : R0) (l0 : L0) => fxcut l0 r0 }}) =>
      lt_r fyR fyL (fun (r0 : R') (l0 : L') => fycut l0 r0) fxR fxL
        (fun (r0 : R0) (l0 : L0) => fxcut l0 r0) l dp)
     (fun (L0 R0 : Type) (s : InSort S L0 R0) (xL0 : L0 -> GenNo S)
        (xR0 : R0 -> GenNo S) (_ : forall (l : L0) (r0 : R0), xL0 l < xR0 r0)
        (fxL : L0 -> No) (fxR : R0 -> No)
        (fxcut : forall (l : L0) (r0 : R0), 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 : R0) (_ : xR0 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 : R0) (l : L0) => 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 (L0 R0 : Type) (s : InSort S L0 R0)
                    (xL0 : L0 -> GenNo S) (xR0 : R0 -> GenNo S)
                    (_ : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
                    (fxL : L0 -> No) (fxR : R0 -> No)
                    (fxcut : forall (l0 : L0) (r : R0), fxR r < fxL l0) =>
                  {{ fxR | fxL//fun (r : R0) (l0 : L0) => fxcut l0 r }})
                 (fun (a b : No) (H0 : b <= a) (H1 : a <= b) =>
                  path_No a b H1 H0)
                 (fun (L0 R0 : Type) (s : InSort S L0 R0)
                    (xL0 : L0 -> GenNo S) (xR0 : R0 -> GenNo S)
                    (xcut0 : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
                    (fxL : L0 -> No) (fxR : R0 -> No)
                    (fxcut : forall (l0 : L0) (r : R0), 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 : L0, xL0 l0 < {{ yL | yR//ycut }})
                    (dp : forall l0 : L0,
                          {{ fyR | fyL//fun (r : R') (l1 : L') => fycut l1 r }} <
                          fxL l0)
                    (_ : forall r : R', {{ xL0 | xR0//xcut0 }} < yR r)
                    (dq : forall r : R',
                          fyR r <
                          {{ fxR | fxL//fun (r0 : R0) (l0 : L0) =>
                                        fxcut l0 r0 }}) =>
                  le_lr fyR fyL (fun (r : R') (l0 : L') => fycut l0 r) fxR
                    fxL (fun (r : R0) (l0 : L0) => fxcut l0 r)
                    (fun l0 : R' => dq l0) (fun r : L0 => dp r))
                 (fun (L0 R0 : Type) (s : InSort S L0 R0)
                    (xL0 : L0 -> GenNo S) (xR0 : R0 -> GenNo S)
                    (xcut0 : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
                    (fxL : L0 -> No) (fxR : R0 -> No)
                    (fxcut : forall (l0 : L0) (r : R0), 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') (_ : {{ xL0 | xR0//xcut0 }} <= yL l0)
                    (dp : fyL l0 <=
                          {{ fxR | fxL//fun (r : R0) (l1 : L0) => fxcut l1 r }}) =>
                  lt_r fyR fyL (fun (r : R') (l1 : L') => fycut l1 r) fxR fxL
                    (fun (r : R0) (l1 : L0) => fxcut l1 r) l0 dp)
                 (fun (L0 R0 : Type) (s : InSort S L0 R0)
                    (xL0 : L0 -> GenNo S) (xR0 : R0 -> GenNo S)
                    (_ : forall (l0 : L0) (r : R0), xL0 l0 < xR0 r)
                    (fxL : L0 -> No) (fxR : R0 -> No)
                    (fxcut : forall (l0 : L0) (r : R0), 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 : R0) (_ : xR0 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 : R0) (l0 : L0) => 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 (L0 R0 : Type) (s : InSort S L0 R0)
                               (xL0 : L0 -> GenNo S) 
                               (xR0 : R0 -> GenNo S)
                               (_ : forall (l0 : L0) 
                                    (r0 : R0), xL0 l0 < xR0 r0)
                               (fxL : L0 -> No) (fxR : R0 -> No)
                               (fxcut : forall (l0 : L0) 
                                        (r0 : R0), 
                                        fxR r0 < fxL l0) =>
                             {{ fxR | fxL//fun (r0 : R0) (l0 : L0) =>
                                           fxcut l0 r0 }})
                            (fun (a b : No) (H0 : b <= a) (H1 : a <= b) =>
                             path_No a b H1 H0)
                            (fun (L0 R0 : Type) (s : InSort S L0 R0)
                               (xL0 : L0 -> GenNo S) 
                               (xR0 : R0 -> GenNo S)
                               (xcut0 : forall (l0 : L0) 
                                        (r0 : R0), 
                                        xL0 l0 < xR0 r0)
                               (fxL : L0 -> No) (fxR : R0 -> No)
                               (fxcut : forall (l0 : L0) 
                                        (r0 : R0), 
                                        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 : L0,
                                    xL0 l0 < {{ yL | yR//ycut }})
                               (dp : forall l0 : L0,
                                     {{ fyR | fyL//
                                     fun (r0 : R') (l1 : L') => 
                                     fycut l1 r0 }} < 
                                     fxL l0)
                               (_ : forall r0 : R',
                                    {{ xL0 | xR0//xcut0 }} < yR r0)
                               (dq : forall r0 : R',
                                     fyR r0 <
                                     {{ fxR | fxL//
                                     fun (r1 : R0) (l0 : L0) => 
                                     fxcut l0 r1 }}) =>
                             le_lr fyR fyL
                               (fun (r0 : R') (l0 : L') => fycut l0 r0) fxR
                               fxL (fun (r0 : R0) (l0 : L0) => fxcut l0 r0)
                               (fun l0 : R' => dq l0) 
                               (fun r0 : L0 => dp r0))
                            (fun (L0 R0 : Type) (s : InSort S L0 R0)
                               (xL0 : L0 -> GenNo S) 
                               (xR0 : R0 -> GenNo S)
                               (xcut0 : forall (l0 : L0) 
                                        (r0 : R0), 
                                        xL0 l0 < xR0 r0)
                               (fxL : L0 -> No) (fxR : R0 -> No)
                               (fxcut : forall (l0 : L0) 
                                        (r0 : R0), 
                                        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')
                               (_ : {{ xL0 | xR0//xcut0 }} <= yL l0)
                               (dp : fyL l0 <=
                                     {{ fxR | fxL//
                                     fun (r0 : R0) (l1 : L0) => 
                                     fxcut l1 r0 }}) =>
                             lt_r fyR fyL
                               (fun (r0 : R') (l1 : L') => fycut l1 r0) fxR
                               fxL (fun (r0 : R0) (l1 : L0) => fxcut l1 r0)
                               l0 dp)
                            (fun (L0 R0 : Type) (s : InSort S L0 R0)
                               (xL0 : L0 -> GenNo S) 
                               (xR0 : R0 -> GenNo S)
                               (_ : forall (l0 : L0) 
                                    (r0 : R0), xL0 l0 < xR0 r0)
                               (fxL : L0 -> No) (fxR : R0 -> No)
                               (fxcut : forall (l0 : L0) 
                                        (r0 : R0), 
                                        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 : R0) (_ : xR0 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 : R0) (l0 : L0) => 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 r0 : Empty => negate (Empty.Empty_rec r0) | 
(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 r0 : Empty => negate (Empty.Empty_rec r0) | 
(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 r0 : Empty => negate (Empty.Empty_rec r0) | 
(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 r0 : Empty => negate (Empty.Empty_rec r0) | 
(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 r0 : Empty => negate (Empty.Empty_rec r0) | 
(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.