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

Local Open Scope path_scope.
Local Open Scope surreal_scope.

(** * Addition of surreal numbers *)

(** Addition requires the option sorts to be closed under finite sums. *)
Class HasAddition (S : OptionSort) :=
  { empty_options :: InSort S Empty Empty
    ; sum_options :: forall L R L' R',
        InSort S L R -> InSort S L' R' -> InSort S (L + L') (R + R')
  }.

Instance hasaddition_maxsort : HasAddition MaxSort
  := { empty_options := tt ;
       sum_options := fun _ _ _ _ _ _ => tt }.

Instance hasaddition_ordsort : HasAddition OrdSort
  := { empty_options := idmap ;
       sum_options := fun _ _ _ _ f g => sum_ind _ f g }.

Instance hasaddition_decsort : HasAddition DecSort.
HasAddition DecSort
Proof.
HasAddition DecSort
  constructor.
InSort DecSort Empty Empty
forall L R L' R' : Type,
InSort DecSort L R ->
InSort DecSort L' R' ->
InSort DecSort (L + L') (R + R')
  -
InSort DecSort Empty Empty exact insort_decsort.
  -
forall L R L' R' : Type,
InSort DecSort L R ->
InSort DecSort L' R' ->
InSort DecSort (L + L') (R + R') intros L R L' R' [? ?] [? ?]; split; exact _.
Qed.

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

  Section Inner.

    Context {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).

    Let A := {g : No -> No &
              (forall x y : No, x <= y -> g x <= g y) *
              (forall x y : No, x < y -> g x < g y)}.

    Context (xL_plus : L -> A) (xR_plus : R -> A)
            (xL_lt_xR_plus : forall (l : L) (r : R) (x : No),
                               (xL_plus l).1 x < (xR_plus r).1 x).

    Definition plus_inner
    : { g : forall (y : No),
              { x_plus_y : No &
                (forall l, (xL_plus l).1 y < x_plus_y) *
                (forall r, x_plus_y < (xR_plus r).1 y) } &
        (forall y z : No, y <= z -> (g y).1 <= (g z).1) *
        (forall y z : No, y <  z -> (g y).1 <  (g z).1) }.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
{g
: forall y : No,
  {x_plus_y : No &
  (forall l : L, (xL_plus l).1 y < x_plus_y) *
  (forall r : R, x_plus_y < (xR_plus r).1 y)} &
(forall y z : No, y <= z -> (g y).1 <= (g z).1) *
(forall y z : No, y < z -> (g y).1 < (g z).1)}
    Proof.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
{g
: forall y : No,
  {x_plus_y : No &
  (forall l : L, (xL_plus l).1 y < x_plus_y) *
  (forall r : R, x_plus_y < (xR_plus r).1 y)} &
(forall y z : No, y <= z -> (g y).1 <= (g z).1) *
(forall y z : No, y < z -> (g y).1 < (g z).1)}
      simple refine (No_ind_package
                (fun y => { x_plus_y : No &
                            (forall l, (xL_plus l).1 y < x_plus_y) *
                            (forall r, x_plus_y < (xR_plus r).1 y) })
                (fun _ _ _ z w => z.1 <= w.1)
                (fun _ _ _ z w => z.1 < w.1)
                _ _ _ _ _).
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL : L0 -> GenNo S) (xR : R0 -> GenNo S)
(xcut : forall (l : L0) (r : R0), xL l < xR r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR r)),
(forall (l : L0) (r : R0),
 (fun (x y : GenNo S) (_ : x < y)
    (z : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           x)
    (w : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           y) => z.1 < w.1) (xL l) (xR r) (xcut l r)
   (fxL l) (fxR r)) ->
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ xL | xR//xcut }}
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (x y : GenNo S)
(a : (fun y0 : GenNo S =>
      {x_plus_y : No &
      (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
      (forall r : R, x_plus_y < (xR_plus r).1 y0)}) x)
(b : (fun y0 : GenNo S =>
      {x_plus_y : No &
      (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
      (forall r : R, x_plus_y < (xR_plus r).1 y0)}) y)
(p : x <= y) (q : y <= x),
(fun (x0 y0 : GenNo S) (_ : x0 <= y0)
   (z : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          x0)
   (w : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          y0) => z.1 <= w.1) x y p a b ->
(fun (x0 y0 : GenNo S) (_ : x0 <= y0)
   (z : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          x0)
   (w : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          y0) => z.1 <= w.1) y x q b a ->
transport
  (fun y0 : GenNo S =>
   {x_plus_y : No &
   (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
   (forall r : R, x_plus_y < (xR_plus r).1 y0)})
  (path_No x y p q) a = b
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL0 : L0 -> GenNo S) (xR0 : R0 -> GenNo S)
(xcut0 : forall (l : L0) (r : R0), xL0 l < xR0 r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL0 l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR0 r))
(fxcut : forall (l : L0) 
         (r : R0),
         (fun (x y : GenNo S) 
            (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (xL0 l) 
           (xR0 r) (xcut0 l r) 
           (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 : forall l : L',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (yL l))
(fyR : forall r : R',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (yR r))
(fycut : forall (l : L') 
         (r : R'),
         (fun (x y : GenNo S) 
            (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (yL l) 
           (yR r) (ycut l r) 
           (fyL l) (fyR r))
(p : forall l : L0, xL0 l < {{ yL | yR//ycut }}),
(forall l : L0,
 (fun (x y : GenNo S) (_ : x < y)
    (z : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r : R, x_plus_y < (xR_plus r).1 y0)})
           x)
    (w : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r : R, x_plus_y < (xR_plus r).1 y0)})
           y) => z.1 < w.1) 
   (xL0 l) {{ yL | yR//ycut }} 
   (p l) (fxL l)
   (?dcut L' R' s' yL yR ycut fyL fyR fycut)) ->
forall
q : forall r : R', {{ xL0 | xR0//xcut0 }} < yR r,
(forall r : R',
 (fun (x y : GenNo S) (_ : x < y)
    (z : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           x)
    (w : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           y) => z.1 < w.1) {{ xL0 | xR0//xcut0 }}
   (yR r) (q r)
   (?dcut L0 R0 s xL0 xR0 xcut0 fxL fxR fxcut) 
   (fyR r)) ->
(fun (x y : GenNo S) (_ : x <= y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          y) => z.1 <= w.1) {{ xL0 | xR0//xcut0 }}
  {{ yL | yR//ycut }}
  (le_lr xL0 xR0 xcut0 yL yR ycut p q)
  (?dcut L0 R0 s xL0 xR0 xcut0 fxL fxR fxcut)
  (?dcut L' R' s' yL yR ycut fyL fyR fycut)
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL0 : L0 -> GenNo S) (xR0 : R0 -> GenNo S)
(xcut0 : forall (l : L0) (r : R0), xL0 l < xR0 r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL0 l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR0 r))
(fxcut : forall (l : L0) 
         (r : R0),
         (fun (x y : GenNo S) 
            (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (xL0 l) 
           (xR0 r) (xcut0 l r) 
           (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 : forall l : L',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (yL l))
(fyR : forall r : R',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (yR r))
(fycut : forall (l : L') 
         (r : R'),
         (fun (x y : GenNo S) 
            (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (yL l) 
           (yR r) (ycut l r) 
           (fyL l) (fyR r)) 
(l : L') (p : {{ xL0 | xR0//xcut0 }} <= yL l),
(fun (x y : GenNo S) (_ : x <= y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          y) => z.1 <= w.1) {{ xL0 | xR0//xcut0 }}
  (yL l) p (?dcut L0 R0 s xL0 xR0 xcut0 fxL fxR fxcut)
  (fyL l) ->
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          y) => z.1 < w.1) {{ xL0 | xR0//xcut0 }}
  {{ yL | yR//ycut }}
  (lt_l xL0 xR0 xcut0 yL yR ycut l p)
  (?dcut L0 R0 s xL0 xR0 xcut0 fxL fxR fxcut)
  (?dcut L' R' s' yL yR ycut fyL fyR fycut)
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL0 : L0 -> GenNo S) (xR0 : R0 -> GenNo S)
(xcut0 : forall (l : L0) (r : R0), xL0 l < xR0 r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL0 l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR0 r))
(fxcut : forall (l : L0) 
         (r : R0),
         (fun (x y : GenNo S) 
            (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (xL0 l) 
           (xR0 r) (xcut0 l r) 
           (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 : forall l : L',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (yL l))
(fyR : forall r : R',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (yR r))
(fycut : forall (l : L') 
         (r : R'),
         (fun (x y : GenNo S) 
            (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall 
                   l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall 
                   r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (yL l) 
           (yR r) (ycut l r) 
           (fyL l) (fyR r)) 
(r : R0) (p : xR0 r <= {{ yL | yR//ycut }}),
(fun (x y : GenNo S) (_ : x <= y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          y) => z.1 <= w.1) 
  (xR0 r) {{ yL | yR//ycut }} p 
  (fxR r) (?dcut L' R' s' yL yR ycut fyL fyR fycut) ->
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          y) => z.1 < w.1) {{ xL0 | xR0//xcut0 }}
  {{ yL | yR//ycut }}
  (lt_r xL0 xR0 xcut0 yL yR ycut r p)
  (?dcut L0 R0 s xL0 xR0 xcut0 fxL fxR fxcut)
  (?dcut L' R' s' yL yR ycut fyL fyR fycut)
      -
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL : L0 -> GenNo S) (xR : R0 -> GenNo S)
(xcut : forall (l : L0) (r : R0), xL l < xR r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR r)),
(forall (l : L0) (r : R0),
 (fun (x y : GenNo S) (_ : x < y)
    (z : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           x)
    (w : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           y) => z.1 < w.1) (xL l) (xR r) (xcut l r)
   (fxL l) (fxR r)) ->
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ xL | xR//xcut }} intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}
        pose (L'' := L + L').
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}  pose (R'' := R + R').
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}
        pose (zL := sum_ind (fun _ => No)
                            (fun l => (xL_plus l).1 {{ yL | yR // ycut }})
                            (fun l => (x_plus_yL l).1)
                    : L'' -> No).
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}
        pose (zR := sum_ind (fun _ => No)
                            (fun r => (xR_plus r).1 {{ yL | yR // ycut }})
                            (fun r => (x_plus_yR r).1)
                    : R'' -> No).
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}
        assert (zcut : forall (l:L'') (r:R''), zL l < zR r).
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
forall (l : L'') (r : R''), zL l < zR r
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}
        {
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
forall (l : L'') (r : R''), zL l < zR r abstract (
          intros [l|l] [r|r]; cbn;
          [ apply xL_lt_xR_plus
          | transitivity ((xL_plus l).1 (yR r));
            [ apply (snd (xL_plus l).2), lt_ropt; exact _
            | exact (fst (x_plus_yR r).2 l) ]
          | transitivity ((xR_plus r).1 (yL l));
            [ exact (snd (x_plus_yL l).2 r)
            | apply (snd (xR_plus r).2), lt_lopt; exact _ ]
          | apply x_plus_yL_lt_yR ]). }
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}
        assert (InSort S L'' R'') by (apply sum_options; exact _).
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
X: InSort S L'' R''
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  {{ yL | yR//ycut }}
        exists ({{ zL | zR // zcut }}); split.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
X: InSort S L'' R''
forall l : L,
(xL_plus l).1 {{ yL | yR//ycut }} <
{{ zL | zR//zcut }}
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
X: InSort S L'' R''
forall r : R,
{{ zL | zR//zcut }} <
(xR_plus r).1 {{ yL | yR//ycut }}
        +
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
X: InSort S L'' R''
forall l : L,
(xL_plus l).1 {{ yL | yR//ycut }} <
{{ zL | zR//zcut }} intros l.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
X: InSort S L'' R''
l: L
(xL_plus l).1 {{ yL | yR//ycut }} <
{{ zL | zR//zcut }}
          exact (lt_lopt zL zR zcut (inl l)).
        +
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
X: InSort S L'' R''
forall r : R,
{{ zL | zR//zcut }} <
(xR_plus r).1 {{ yL | yR//ycut }} intros r.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
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
x_plus_yL: forall l : L',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l0 : L,
  (xL_plus l0).1 y < x_plus_y) *
 (forall r : R, x_plus_y < (xR_plus r).1 y)})
  (yL l)
x_plus_yR: forall r : R',
(fun y : GenNo S =>
 {x_plus_y : No &
 (forall l : L, (xL_plus l).1 y < x_plus_y) *
 (forall r0 : R,
  x_plus_y < (xR_plus r0).1 y)}) 
  (yR r)
x_plus_yL_lt_yR: forall (l : L') (r : R'),
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L,
          (xL_plus l0).1 y0 <
          x_plus_y) *
         (forall r0 : R,
          x_plus_y <
          (xR_plus r0).1 y0)}) y) =>
 z.1 < w.1) (yL l) (yR r) 
  (ycut l r) (x_plus_yL l)
  (x_plus_yR r)
L'':= L + L': Type
R'':= R + R': Type
zL:= sum_ind (fun _ : L + L' => No)
  (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
  (fun l : L' => (x_plus_yL l).1)
:
L'' -> No: L'' -> No
zR:= sum_ind (fun _ : R + R' => No)
  (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
  (fun r : R' => (x_plus_yR r).1)
:
R'' -> No: R'' -> No
zcut: forall (l : L'') (r : R''), zL l < zR r
X: InSort S L'' R''
r: R
{{ zL | zR//zcut }} <
(xR_plus r).1 {{ yL | yR//ycut }}
          exact (lt_ropt zL zR zcut (inl r)).
      -
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (x y : GenNo S)
(a : (fun y0 : GenNo S =>
      {x_plus_y : No &
      (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
      (forall r : R, x_plus_y < (xR_plus r).1 y0)}) x)
(b : (fun y0 : GenNo S =>
      {x_plus_y : No &
      (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
      (forall r : R, x_plus_y < (xR_plus r).1 y0)}) y)
(p : x <= y) (q : y <= x),
(fun (x0 y0 : GenNo S) (_ : x0 <= y0)
   (z : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          x0)
   (w : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          y0) => z.1 <= w.1) x y p a b ->
(fun (x0 y0 : GenNo S) (_ : x0 <= y0)
   (z : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          x0)
   (w : (fun y1 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y1 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y1)})
          y0) => z.1 <= w.1) y x q b a ->
transport
  (fun y0 : GenNo S =>
   {x_plus_y : No &
   (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
   (forall r : R, x_plus_y < (xR_plus r).1 y0)})
  (path_No x y p q) a = b abstract (
        intros x y [a ?] [b ?] p q r s;
        rewrite transport_sigma; cbn in *;
        apply path_sigma_hprop, path_No; cbn;
        rewrite transport_const; assumption).
      -
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL : L0 -> GenNo S) (xR : R0 -> GenNo S)
(xcut : forall (l : L0) (r : R0), xL l < xR r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR r))
(fxcut : forall (l : L0) (r : R0),
         (fun (x y : GenNo S) (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (xL l) (xR r) (xcut l r)
           (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 : forall l : L',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (yL l))
(fyR : forall r : R',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (yR r))
(fycut : forall (l : L') (r : R'),
         (fun (x y : GenNo S) (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (yL l) (yR r) (ycut l r)
           (fyL l) (fyR r))
(p : forall l : L0, xL l < {{ yL | yR//ycut }}),
(forall l : L0,
 (fun (x y : GenNo S) (_ : x < y)
    (z : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r : R, x_plus_y < (xR_plus r).1 y0)})
           x)
    (w : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
          (forall r : R, x_plus_y < (xR_plus r).1 y0)})
           y) => z.1 < w.1) (xL l) {{ yL | yR//ycut }}
   (p l) (fxL l)
   ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
       (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
       (ycut0 : forall (l0 : L'0) (r : R'0),
                yL0 l0 < yR0 r)
       (x_plus_yL : forall l0 : L'0,
                    (fun y : GenNo S =>
                     {x_plus_y : No &
                     (forall l1 : L,
                      (xL_plus l1).1 y < x_plus_y) *
                     (forall r : R,
                      x_plus_y < (xR_plus r).1 y)})
                      (yL0 l0))
       (x_plus_yR : forall r : R'0,
                    (fun y : GenNo S =>
                     {x_plus_y : No &
                     (forall l0 : L,
                      (xL_plus l0).1 y < x_plus_y) *
                     (forall r0 : R,
                      x_plus_y < (xR_plus r0).1 y)})
                      (yR0 r))
       (x_plus_yL_lt_yR : forall (l0 : L'0) (r : R'0),
                          (fun (x y : GenNo S)
                             (_ : x < y)
                             (z : (fun y0 : GenNo S =>
                                   {x_plus_y : No &
                                   (forall l1 : L,
                                    (...).1 y0 <
                                    x_plus_y) *
                                   (forall r0 : R,
                                    x_plus_y <
                                    (...).1 y0)}) x)
                             (w : (fun y0 : GenNo S =>
                                   {x_plus_y : No &
                                   (forall l1 : L,
                                    (...).1 y0 <
                                    x_plus_y) *
                                   (forall r0 : R,
                                    x_plus_y <
                                    (...).1 y0)}) y)
                           => z.1 < w.1) (yL0 l0)
                            (yR0 r) (ycut0 l0 r)
                            (x_plus_yL l0)
                            (x_plus_yR r)) =>
     let L'' := L + L'0 in
     let R'' := R + R'0 in
     let zL :=
       sum_ind (fun _ : L + L'0 => No)
         (fun l0 : L =>
          (xL_plus l0).1 {{ yL0 | yR0//ycut0 }})
         (fun l0 : L'0 => (x_plus_yL l0).1)
       :
       L'' -> No in
     let zR :=
       sum_ind (fun _ : R + R'0 => No)
         (fun r : R =>
          (xR_plus r).1 {{ yL0 | yR0//ycut0 }})
         (fun r : R'0 => (x_plus_yR r).1)
       :
       R'' -> No in
     let zcut :=
       plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
         x_plus_yL x_plus_yR x_plus_yL_lt_yR in
     let X := sum_options L R L'0 R'0 Sx s0 in
     ({{ zL | zR//zcut }};
     (fun l0 : L => lt_lopt zL zR zcut (inl l0),
     fun r : R => lt_ropt zL zR zcut (inl r)))) L' R'
      s' yL yR ycut fyL fyR fycut)) ->
forall q : forall r : R', {{ xL | xR//xcut }} < yR r,
(forall r : R',
 (fun (x y : GenNo S) (_ : x < y)
    (z : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           x)
    (w : (fun y0 : GenNo S =>
          {x_plus_y : No &
          (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
          (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
           y) => z.1 < w.1) {{ xL | xR//xcut }} (yR r)
   (q r)
   ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
       (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
       (ycut0 : forall (l : L'0) (r0 : R'0),
                yL0 l < yR0 r0)
       (x_plus_yL : forall l : L'0,
                    (fun y : GenNo S =>
                     {x_plus_y : No &
                     (forall l0 : L,
                      (xL_plus l0).1 y < x_plus_y) *
                     (forall r0 : R,
                      x_plus_y < (xR_plus r0).1 y)})
                      (yL0 l))
       (x_plus_yR : forall r0 : R'0,
                    (fun y : GenNo S =>
                     {x_plus_y : No &
                     (forall l : L,
                      (xL_plus l).1 y < x_plus_y) *
                     (forall r1 : R,
                      x_plus_y < (xR_plus r1).1 y)})
                      (yR0 r0))
       (x_plus_yL_lt_yR : forall (l : L'0) (r0 : R'0),
                          (fun (x y : GenNo S)
                             (_ : x < y)
                             (z : (fun y0 : GenNo S =>
                                   {x_plus_y : No &
                                   (forall l0 : L,
                                    ... < x_plus_y) *
                                   (forall r1 : R,
                                    x_plus_y < ...)})
                                    x)
                             (w : (fun y0 : GenNo S =>
                                   {x_plus_y : No &
                                   (forall l0 : L,
                                    ... < x_plus_y) *
                                   (forall r1 : R,
                                    x_plus_y < ...)})
                                    y) => z.1 < w.1)
                            (yL0 l) (yR0 r0)
                            (ycut0 l r0) (x_plus_yL l)
                            (x_plus_yR r0)) =>
     let L'' := L + L'0 in
     let R'' := R + R'0 in
     let zL :=
       sum_ind (fun _ : L + L'0 => No)
         (fun l : L =>
          (xL_plus l).1 {{ yL0 | yR0//ycut0 }})
         (fun l : L'0 => (x_plus_yL l).1)
       :
       L'' -> No in
     let zR :=
       sum_ind (fun _ : R + R'0 => No)
         (fun r0 : R =>
          (xR_plus r0).1 {{ yL0 | yR0//ycut0 }})
         (fun r0 : R'0 => (x_plus_yR r0).1)
       :
       R'' -> No in
     let zcut :=
       plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
         x_plus_yL x_plus_yR x_plus_yL_lt_yR in
     let X := sum_options L R L'0 R'0 Sx s0 in
     ({{ zL | zR//zcut }};
     (fun l : L => lt_lopt zL zR zcut (inl l),
     fun r0 : R => lt_ropt zL zR zcut (inl r0)))) L0
      R0 s xL xR xcut fxL fxR fxcut) (fyR r)) ->
(fun (x y : GenNo S) (_ : x <= y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          y) => z.1 <= w.1) {{ xL | xR//xcut }}
  {{ yL | yR//ycut }}
  (le_lr xL xR xcut yL yR ycut p q)
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l : L'0) (r : R'0),
               yL0 l < yR0 r)
      (x_plus_yL : forall l : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 y)})
                     (yL0 l))
      (x_plus_yR : forall r : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yR0 r))
      (x_plus_yL_lt_yR : forall (l : L'0) (r : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (...).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (...).1 y0)}) x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (...).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (...).1 y0)}) y) =>
                          z.1 < w.1) (yL0 l) (yR0 r)
                           (ycut0 l r) (x_plus_yL l)
                           (x_plus_yR r)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l : L =>
         (xL_plus l).1 {{ yL0 | yR0//ycut0 }})
        (fun l : L'0 => (x_plus_yL l).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r : R =>
         (xR_plus r).1 {{ yL0 | yR0//ycut0 }})
        (fun r : R'0 => (x_plus_yR r).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l : L => lt_lopt zL zR zcut (inl l),
    fun r : R => lt_ropt zL zR zcut (inl r)))) L0 R0 s
     xL xR xcut fxL fxR fxcut)
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l : L'0) (r : R'0),
               yL0 l < yR0 r)
      (x_plus_yL : forall l : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 y)})
                     (yL0 l))
      (x_plus_yR : forall r : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yR0 r))
      (x_plus_yL_lt_yR : forall (l : L'0) (r : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (...).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (...).1 y0)}) x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (...).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (...).1 y0)}) y) =>
                          z.1 < w.1) (yL0 l) (yR0 r)
                           (ycut0 l r) (x_plus_yL l)
                           (x_plus_yR r)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l : L =>
         (xL_plus l).1 {{ yL0 | yR0//ycut0 }})
        (fun l : L'0 => (x_plus_yL l).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r : R =>
         (xR_plus r).1 {{ yL0 | yR0//ycut0 }})
        (fun r : R'0 => (x_plus_yR r).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l : L => lt_lopt zL zR zcut (inl l),
    fun r : R => lt_ropt zL zR zcut (inl r)))) L' R'
     s' yL yR ycut fyL fyR fycut) abstract (
        intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR
               L'' R'' ? zL zR zcut x_plus_zL x_plus_zR x_plus_zL_lt_zR
               yL_lt_z x_plus_yL_lt_z y_lt_zR x_plus_y_lt_zR;
        cbn in *;
        apply le_lr; [ intros [l|l] | intros [r|r] ]; cbn;
        [ refine (le_lt_trans (fst (xL_plus l).2 _ {{ zL | zR // zcut}} _) _);
          [ by (apply le_lr; assumption)
          | exact (lt_lopt _ _ _ (inl l)) ]
        | exact (x_plus_yL_lt_z l)
        | refine (lt_le_trans _
                    (fst (xR_plus r).2 {{ yL | yR // ycut}} _ _));
          [ exact (lt_ropt _ _ _ (inl r))
          | by (apply le_lr; assumption) ]
        | exact (x_plus_y_lt_zR r) ] ).
      -
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL : L0 -> GenNo S) (xR : R0 -> GenNo S)
(xcut : forall (l : L0) (r : R0), xL l < xR r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR r))
(fxcut : forall (l : L0) (r : R0),
         (fun (x y : GenNo S) (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (xL l) (xR r) (xcut l r)
           (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 : forall l : L',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (yL l))
(fyR : forall r : R',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (yR r))
(fycut : forall (l : L') (r : R'),
         (fun (x y : GenNo S) (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (yL l) (yR r) (ycut l r)
           (fyL l) (fyR r)) (l : L')
(p : {{ xL | xR//xcut }} <= yL l),
(fun (x y : GenNo S) (_ : x <= y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          y) => z.1 <= w.1) {{ xL | xR//xcut }} (yL l)
  p
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l0 : L'0) (r : R'0),
               yL0 l0 < yR0 r)
      (x_plus_yL : forall l0 : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l1 : L,
                     (xL_plus l1).1 y < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 y)})
                     (yL0 l0))
      (x_plus_yR : forall r : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yR0 r))
      (x_plus_yL_lt_yR : forall (l0 : L'0) (r : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   (xL_plus l1).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (xR_plus r0).1 y0)})
                                   x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   (xL_plus l1).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (xR_plus r0).1 y0)})
                                   y) => z.1 < w.1)
                           (yL0 l0) (yR0 r)
                           (ycut0 l0 r) (x_plus_yL l0)
                           (x_plus_yR r)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l0 : L =>
         (xL_plus l0).1 {{ yL0 | yR0//ycut0 }})
        (fun l0 : L'0 => (x_plus_yL l0).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r : R =>
         (xR_plus r).1 {{ yL0 | yR0//ycut0 }})
        (fun r : R'0 => (x_plus_yR r).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l0 : L => lt_lopt zL zR zcut (inl l0),
    fun r : R => lt_ropt zL zR zcut (inl r)))) L0 R0 s
     xL xR xcut fxL fxR fxcut) (fyL l) ->
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l0 : L, (xL_plus l0).1 y0 < x_plus_y) *
         (forall r : R, x_plus_y < (xR_plus r).1 y0)})
          y) => z.1 < w.1) {{ xL | xR//xcut }}
  {{ yL | yR//ycut }} (lt_l xL xR xcut yL yR ycut l p)
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l0 : L'0) (r : R'0),
               yL0 l0 < yR0 r)
      (x_plus_yL : forall l0 : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l1 : L,
                     (xL_plus l1).1 y < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 y)})
                     (yL0 l0))
      (x_plus_yR : forall r : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yR0 r))
      (x_plus_yL_lt_yR : forall (l0 : L'0) (r : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   (xL_plus l1).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (xR_plus r0).1 y0)})
                                   x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   (xL_plus l1).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (xR_plus r0).1 y0)})
                                   y) => z.1 < w.1)
                           (yL0 l0) (yR0 r)
                           (ycut0 l0 r) (x_plus_yL l0)
                           (x_plus_yR r)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l0 : L =>
         (xL_plus l0).1 {{ yL0 | yR0//ycut0 }})
        (fun l0 : L'0 => (x_plus_yL l0).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r : R =>
         (xR_plus r).1 {{ yL0 | yR0//ycut0 }})
        (fun r : R'0 => (x_plus_yR r).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l0 : L => lt_lopt zL zR zcut (inl l0),
    fun r : R => lt_ropt zL zR zcut (inl r)))) L0 R0 s
     xL xR xcut fxL fxR fxcut)
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l0 : L'0) (r : R'0),
               yL0 l0 < yR0 r)
      (x_plus_yL : forall l0 : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l1 : L,
                     (xL_plus l1).1 y < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 y)})
                     (yL0 l0))
      (x_plus_yR : forall r : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yR0 r))
      (x_plus_yL_lt_yR : forall (l0 : L'0) (r : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   (xL_plus l1).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (xR_plus r0).1 y0)})
                                   x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   (xL_plus l1).1 y0 <
                                   x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y <
                                   (xR_plus r0).1 y0)})
                                   y) => z.1 < w.1)
                           (yL0 l0) (yR0 r)
                           (ycut0 l0 r) (x_plus_yL l0)
                           (x_plus_yR r)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l0 : L =>
         (xL_plus l0).1 {{ yL0 | yR0//ycut0 }})
        (fun l0 : L'0 => (x_plus_yL l0).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r : R =>
         (xR_plus r).1 {{ yL0 | yR0//ycut0 }})
        (fun r : R'0 => (x_plus_yR r).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l0 : L => lt_lopt zL zR zcut (inl l0),
    fun r : R => lt_ropt zL zR zcut (inl r)))) L' R'
     s' yL yR ycut fyL fyR fycut) abstract (
        intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR
               L'' R'' ? zL zR zcut x_plus_zL x_plus_zR x_plus_zL_lt_zR
               l y_le_zL x_plus_y_le_zL; cbn;
        apply lt_l with (inr l);
        exact x_plus_y_le_zL ).
      -
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
forall (L0 R0 : Type) (s : InSort S L0 R0)
(xL : L0 -> GenNo S) (xR : R0 -> GenNo S)
(xcut : forall (l : L0) (r : R0), xL l < xR r)
(fxL : forall l : L0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (xL l))
(fxR : forall r : R0,
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (xR r))
(fxcut : forall (l : L0) (r : R0),
         (fun (x y : GenNo S) (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (xL l) (xR r) (xcut l r)
           (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 : forall l : L',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l0 : L, (xL_plus l0).1 y < x_plus_y) *
        (forall r : R, x_plus_y < (xR_plus r).1 y)})
         (yL l))
(fyR : forall r : R',
       (fun y : GenNo S =>
        {x_plus_y : No &
        (forall l : L, (xL_plus l).1 y < x_plus_y) *
        (forall r0 : R, x_plus_y < (xR_plus r0).1 y)})
         (yR r))
(fycut : forall (l : L') (r : R'),
         (fun (x y : GenNo S) (_ : x < y)
            (z : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) x)
            (w : (fun y0 : GenNo S =>
                  {x_plus_y : No &
                  (forall l0 : L,
                   (xL_plus l0).1 y0 < x_plus_y) *
                  (forall r0 : R,
                   x_plus_y < (xR_plus r0).1 y0)}) y)
          => z.1 < w.1) (yL l) (yR r) (ycut l r)
           (fyL l) (fyR r)) (r : R0)
(p : xR r <= {{ yL | yR//ycut }}),
(fun (x y : GenNo S) (_ : x <= y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          y) => z.1 <= w.1) (xR r) {{ yL | yR//ycut }}
  p (fxR r)
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l : L'0) (r0 : R'0),
               yL0 l < yR0 r0)
      (x_plus_yL : forall l : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yL0 l))
      (x_plus_yR : forall r0 : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 y < x_plus_y) *
                    (forall r1 : R,
                     x_plus_y < (xR_plus r1).1 y)})
                     (yR0 r0))
      (x_plus_yL_lt_yR : forall (l : L'0) (r0 : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (xL_plus l0).1 y0 <
                                   x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y <
                                   (xR_plus r1).1 y0)})
                                   x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (xL_plus l0).1 y0 <
                                   x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y <
                                   (xR_plus r1).1 y0)})
                                   y) => z.1 < w.1)
                           (yL0 l) (yR0 r0)
                           (ycut0 l r0) (x_plus_yL l)
                           (x_plus_yR r0)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l : L =>
         (xL_plus l).1 {{ yL0 | yR0//ycut0 }})
        (fun l : L'0 => (x_plus_yL l).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r0 : R =>
         (xR_plus r0).1 {{ yL0 | yR0//ycut0 }})
        (fun r0 : R'0 => (x_plus_yR r0).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l : L => lt_lopt zL zR zcut (inl l),
    fun r0 : R => lt_ropt zL zR zcut (inl r0)))) L' R'
     s' yL yR ycut fyL fyR fycut) ->
(fun (x y : GenNo S) (_ : x < y)
   (z : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          x)
   (w : (fun y0 : GenNo S =>
         {x_plus_y : No &
         (forall l : L, (xL_plus l).1 y0 < x_plus_y) *
         (forall r0 : R, x_plus_y < (xR_plus r0).1 y0)})
          y) => z.1 < w.1) {{ xL | xR//xcut }}
  {{ yL | yR//ycut }} (lt_r xL xR xcut yL yR ycut r p)
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l : L'0) (r0 : R'0),
               yL0 l < yR0 r0)
      (x_plus_yL : forall l : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yL0 l))
      (x_plus_yR : forall r0 : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 y < x_plus_y) *
                    (forall r1 : R,
                     x_plus_y < (xR_plus r1).1 y)})
                     (yR0 r0))
      (x_plus_yL_lt_yR : forall (l : L'0) (r0 : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (xL_plus l0).1 y0 <
                                   x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y <
                                   (xR_plus r1).1 y0)})
                                   x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (xL_plus l0).1 y0 <
                                   x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y <
                                   (xR_plus r1).1 y0)})
                                   y) => z.1 < w.1)
                           (yL0 l) (yR0 r0)
                           (ycut0 l r0) (x_plus_yL l)
                           (x_plus_yR r0)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l : L =>
         (xL_plus l).1 {{ yL0 | yR0//ycut0 }})
        (fun l : L'0 => (x_plus_yL l).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r0 : R =>
         (xR_plus r0).1 {{ yL0 | yR0//ycut0 }})
        (fun r0 : R'0 => (x_plus_yR r0).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l : L => lt_lopt zL zR zcut (inl l),
    fun r0 : R => lt_ropt zL zR zcut (inl r0)))) L0 R0
     s xL xR xcut fxL fxR fxcut)
  ((fun (L'0 R'0 : Type) (s0 : InSort S L'0 R'0)
      (yL0 : L'0 -> GenNo S) (yR0 : R'0 -> GenNo S)
      (ycut0 : forall (l : L'0) (r0 : R'0),
               yL0 l < yR0 r0)
      (x_plus_yL : forall l : L'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)})
                     (yL0 l))
      (x_plus_yR : forall r0 : R'0,
                   (fun y : GenNo S =>
                    {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 y < x_plus_y) *
                    (forall r1 : R,
                     x_plus_y < (xR_plus r1).1 y)})
                     (yR0 r0))
      (x_plus_yL_lt_yR : forall (l : L'0) (r0 : R'0),
                         (fun (x y : GenNo S)
                            (_ : x < y)
                            (z : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (xL_plus l0).1 y0 <
                                   x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y <
                                   (xR_plus r1).1 y0)})
                                   x)
                            (w : (fun y0 : GenNo S =>
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   (xL_plus l0).1 y0 <
                                   x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y <
                                   (xR_plus r1).1 y0)})
                                   y) => z.1 < w.1)
                           (yL0 l) (yR0 r0)
                           (ycut0 l r0) (x_plus_yL l)
                           (x_plus_yR r0)) =>
    let L'' := L + L'0 in
    let R'' := R + R'0 in
    let zL :=
      sum_ind (fun _ : L + L'0 => No)
        (fun l : L =>
         (xL_plus l).1 {{ yL0 | yR0//ycut0 }})
        (fun l : L'0 => (x_plus_yL l).1)
      :
      L'' -> No in
    let zR :=
      sum_ind (fun _ : R + R'0 => No)
        (fun r0 : R =>
         (xR_plus r0).1 {{ yL0 | yR0//ycut0 }})
        (fun r0 : R'0 => (x_plus_yR r0).1)
      :
      R'' -> No in
    let zcut :=
      plus_inner_subproof L'0 R'0 s0 yL0 yR0 ycut0
        x_plus_yL x_plus_yR x_plus_yL_lt_yR in
    let X := sum_options L R L'0 R'0 Sx s0 in
    ({{ zL | zR//zcut }};
    (fun l : L => lt_lopt zL zR zcut (inl l),
    fun r0 : R => lt_ropt zL zR zcut (inl r0)))) L' R'
     s' yL yR ycut fyL fyR fycut) abstract (
        intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR
               L'' R'' ? zL zR zcut x_plus_zL x_plus_zR x_plus_zL_lt_zR
               r yR_le_z x_plus_yR_le_z; cbn;
        apply lt_r with (inr r);
        exact x_plus_yR_le_z).
    Defined.

    (** We now prove a computation law for [plus_inner].  It holds definitionally, so we would like to prove it with just [:= 1] and then rewrite along it later, as we did above.  However, there is a subtlety in that the output should be a surreal defined by a cut, which in particular includes a proof of cut-ness, and that proof is rather long, so we would not like to see it in the type of this lemma.  Thus, instead we assert only that there *exists* some proof of cut-ness and an equality. *)
    Definition plus_inner_cut
               {L' R' : Type@{i} } {Sy : InSort S L' R'}
               (yL : L' -> No) (yR : R' -> No)
               (ycut : forall (l : L') (r : R'), yL l < yR r)
    : let L'' := L + L' in
      let R'' := R + R' in
      let zL := sum_ind (fun _ => No)
                        (fun l => (xL_plus l).1 {{ yL | yR // ycut }})
                        (fun l => (plus_inner.1 (yL l)).1)
                : L'' -> No in
      let zR := sum_ind (fun _ => No)
                        (fun r => (xR_plus r).1 {{ yL | yR // ycut }})
                        (fun r => (plus_inner.1 (yR r)).1)
                : R'' -> No in
      let Sz := sum_options L R L' R' _ _ in
      { zcut : forall (l:L'') (r:R''), zL l < zR r &
        (plus_inner.1 {{ yL | yR // ycut }}).1 = (@No_cut _ _ _ Sz zL zR zcut) }.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
L', R': Type
Sy: InSort S L' R'
yL: L' -> No
yR: R' -> No
ycut: forall (l : L') (r : R'), yL l < yR r
let L'' := L + L' in
let R'' := R + R' in
let zL :=
  sum_ind (fun _ : L + L' => No)
    (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
    (fun l : L' => (plus_inner.1 (yL l)).1) in
let zR :=
  sum_ind (fun _ : R + R' => No)
    (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
    (fun r : R' => (plus_inner.1 (yR r)).1) in
let Sz := sum_options L R L' R' Sx Sy in
{zcut : forall (l : L'') (r : R''), zL l < zR r &
(plus_inner.1 {{ yL | yR//ycut }}).1 =
{{ zL | zR//zcut }}}
    Proof.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
L', R': Type
Sy: InSort S L' R'
yL: L' -> No
yR: R' -> No
ycut: forall (l : L') (r : R'), yL l < yR r
let L'' := L + L' in
let R'' := R + R' in
let zL :=
  sum_ind (fun _ : L + L' => No)
    (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
    (fun l : L' => (plus_inner.1 (yL l)).1) in
let zR :=
  sum_ind (fun _ : R + R' => No)
    (fun r : R => (xR_plus r).1 {{ yL | yR//ycut }})
    (fun r : R' => (plus_inner.1 (yR r)).1) in
let Sz := sum_options L R L' R' Sx Sy in
{zcut : forall (l : L'') (r : R''), zL l < zR r &
(plus_inner.1 {{ yL | yR//ycut }}).1 =
{{ zL | zR//zcut }}}
      (** Now we tell Coq that we want the equality to be definitional, and let it figure out what the proof of cut-ness has to be. *)
      eexists.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
L', R': Type
Sy: InSort S L' R'
yL: L' -> No
yR: R' -> No
ycut: forall (l : L') (r : R'), yL l < yR r
(plus_inner.1 {{ yL | yR//ycut }}).1 =
{{ sum_ind (fun _ : L + L' => No)
     (fun l : L => (xL_plus l).1 {{ yL | yR//ycut }})
     (fun l : L' => (plus_inner.1 (yL l)).1) | sum_ind
                                                 (fun
                                                 _ : 
                                                 R +
                                                 R' =>
                                                 No)
                                                 (fun
                                                 r : R
                                                 =>
                                                 (xR_plus
                                                 r).1
                                                 {{ yL | yR//ycut }})
                                                 (fun
                                                 r : R'
                                                 =>
                                                 (plus_inner.1
                                                 (yR r)).1)//
?zcut }}
      (** Adding [rel_hnf] here speeds things up considerably, possibly because it puts the terms in a form where the evar can be instantiated without unfolding or reduction, preventing backtracking across the evar instantiation. *)
      rel_hnf.
H: Univalence
S: OptionSort
H0: HasAddition 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
A:= {g : No -> No &
(forall x y : No, x <= y -> g x <= g y) *
(forall x y : No, x < y -> g x < g y)}: Type
xL_plus: L -> A
xR_plus: R -> A
xL_lt_xR_plus: forall (l : L) (r : R) (x : No),
(xL_plus l).1 x < (xR_plus r).1 x
L', R': Type
Sy: InSort S L' R'
yL: L' -> No
yR: R' -> No
ycut: forall (l : L') (r : R'), yL l < yR r
{|
  game_of :=
    opt (L + L') (R + R')
      (sum_options L R L' R' Sx Sy)
      (fun x : L + L' =>
       game_of
         (sum_ind (fun _ : L + L' => No)
            (fun l : L =>
             (xL_plus l).1
               {{ fun l0 : L' =>
                  {|
                    game_of := game_of (yL l0);
                    isno_game_of :=
                      isno_game_of (yL l0)
                  |} | (fun r : R' =>
                        {|
                          game_of := game_of (yR r);
                          isno_game_of :=
                            isno_game_of (yR r)
                        |})//ycut }})
            (fun l : L' =>
             (Core.Surreals.No_ind_internal
                (fun y : GenNo S =>
                 {x_plus_y : No &
                 (forall l0 : L,
                  (xL_plus l0).1 y < x_plus_y) *
                 (forall r : R,
                  x_plus_y < (xR_plus r).1 y)})
                (fun (x0 y : GenNo S) (_ : x0 <= y)
                   (z : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 x0 < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 y < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 y)})
                 => z.1 <= w.1)
                (fun (x0 y : GenNo S) (_ : x0 < y)
                   (z : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 x0 < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 y < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 y)})
                 => z.1 < w.1)
                (fun (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)
                   (x_plus_yL : forall l0 : L',
                                {x_plus_y : No &
                                (forall l1 : L,
                                 (xL_plus l1).1
                                   (yL l0) < x_plus_y) *
                                (forall r : R,
                                 x_plus_y <
                                 (xR_plus r).1 (yL l0))})
                   (x_plus_yR : forall r : R',
                                {x_plus_y : No &
                                (forall l0 : L,
                                 (xL_plus l0).1 (yR r) <
                                 x_plus_y) *
                                (forall r0 : R,
                                 x_plus_y <
                                 (xR_plus r0).1 (yR r))})
                   (x_plus_yL_lt_yR : forall (l0 : L')
                                      (r : R'),
                                      (x_plus_yL l0).1 <
                                      (x_plus_yR r).1)
                 =>
                 let L'' := L + L' in
                 let R'' := R + R' in
                 let zL :=
                   sum_ind (fun _ : L + L' => No)
                     (fun l0 : L =>
                      (xL_plus l0).1
                        {{ yL | yR//ycut }})
                     (fun l0 : L' => (x_plus_yL l0).1)
                   in
                 let zR :=
                   sum_ind (fun _ : R + R' => No)
                     (fun r : R =>
                      (xR_plus r).1
                        {{ yL | yR//ycut }})
                     (fun r : R' => (x_plus_yR r).1)
                   in
                 let zcut :=
                   plus_inner_subproof L' R' s yL yR
                     ycut x_plus_yL x_plus_yR
                     x_plus_yL_lt_yR in
                 let X := sum_options L R L' R' Sx s
                   in
                 ({{ zL | zR//zcut }};
                 (fun l0 : L =>
                  lt_lopt zL zR zcut (...),
                 fun r : R => lt_ropt zL zR zcut (...))))
                plus_inner_subproof0
                plus_inner_subproof1
                plus_inner_subproof2
                plus_inner_subproof3 (game_of (yL l))
                (isno_game_of (yL l))).1) x))
      (fun x : R + R' =>
       game_of
         (sum_ind (fun _ : R + R' => No)
            (fun r : R =>
             (xR_plus r).1
               {{ fun l : L' =>
                  {|
                    game_of := game_of (yL l);
                    isno_game_of :=
                      isno_game_of (yL l)
                  |} | (fun r0 : R' =>
                        {|
                          game_of := game_of (yR r0);
                          isno_game_of :=
                            isno_game_of (yR r0)
                        |})//ycut }})
            (fun r : R' =>
             (Core.Surreals.No_ind_internal
                (fun y : GenNo S =>
                 {x_plus_y : No &
                 (forall l : L,
                  (xL_plus l).1 y < x_plus_y) *
                 (forall r0 : R,
                  x_plus_y < (xR_plus r0).1 y)})
                (fun (x0 y : GenNo S) (_ : x0 <= y)
                   (z : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 x0 < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 y < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 y)})
                 => z.1 <= w.1)
                (fun (x0 y : GenNo S) (_ : x0 < y)
                   (z : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 x0 < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 y < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 y)})
                 => z.1 < w.1)
                (fun (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)
                   (x_plus_yL : forall l : L',
                                {x_plus_y : No &
                                (forall l0 : L,
                                 (xL_plus l0).1 (yL l) <
                                 x_plus_y) *
                                (forall r0 : R,
                                 x_plus_y <
                                 (xR_plus r0).1 (yL l))})
                   (x_plus_yR : forall r0 : R',
                                {x_plus_y : No &
                                (forall l : L,
                                 (xL_plus l).1 (yR r0) <
                                 x_plus_y) *
                                (forall r1 : R,
                                 x_plus_y <
                                 (xR_plus r1).1
                                   (yR r0))})
                   (x_plus_yL_lt_yR : forall (l : L')
                                      (r0 : R'),
                                      (x_plus_yL l).1 <
                                      (x_plus_yR r0).1)
                 =>
                 let L'' := L + L' in
                 let R'' := R + R' in
                 let zL :=
                   sum_ind (fun _ : L + L' => No)
                     (fun l : L =>
                      (xL_plus l).1
                        {{ yL | yR//ycut }})
                     (fun l : L' => (x_plus_yL l).1)
                   in
                 let zR :=
                   sum_ind (fun _ : R + R' => No)
                     (fun r0 : R =>
                      (xR_plus r0).1
                        {{ yL | yR//ycut }})
                     (fun r0 : R' => (x_plus_yR r0).1)
                   in
                 let zcut :=
                   plus_inner_subproof L' R' s yL yR
                     ycut x_plus_yL x_plus_yR
                     x_plus_yL_lt_yR in
                 let X := sum_options L R L' R' Sx s
                   in
                 ({{ zL | zR//zcut }};
                 (fun l : L =>
                  lt_lopt zL zR zcut (...),
                 fun r0 : R =>
                 lt_ropt zL zR zcut (...))))
                plus_inner_subproof0
                plus_inner_subproof1
                plus_inner_subproof2
                plus_inner_subproof3 (game_of (yR r))
                (isno_game_of (yR r))).1) x));
  isno_game_of :=
    isno (L + L') (R + R')
      (sum_options L R L' R' Sx Sy)
      (fun x : L + L' =>
       game_of
         (sum_ind (fun _ : L + L' => No)
            (fun l : L =>
             (xL_plus l).1
               {{ fun l0 : L' =>
                  {|
                    game_of := game_of (yL l0);
                    isno_game_of :=
                      isno_game_of (yL l0)
                  |} | (fun r : R' =>
                        {|
                          game_of := game_of (yR r);
                          isno_game_of :=
                            isno_game_of (yR r)
                        |})//ycut }})
            (fun l : L' =>
             (Core.Surreals.No_ind_internal
                (fun y : GenNo S =>
                 {x_plus_y : No &
                 (forall l0 : L,
                  (xL_plus l0).1 y < x_plus_y) *
                 (forall r : R,
                  x_plus_y < (xR_plus r).1 y)})
                (fun (x0 y : GenNo S) (_ : x0 <= y)
                   (z : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 x0 < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 y < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 y)})
                 => z.1 <= w.1)
                (fun (x0 y : GenNo S) (_ : x0 < y)
                   (z : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 x0 < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 y < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 y)})
                 => z.1 < w.1)
                (fun (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)
                   (x_plus_yL : forall l0 : L',
                                {x_plus_y : No &
                                (forall l1 : L,
                                 (xL_plus l1).1
                                   (yL l0) < x_plus_y) *
                                (forall r : R,
                                 x_plus_y <
                                 (xR_plus r).1 (yL l0))})
                   (x_plus_yR : forall r : R',
                                {x_plus_y : No &
                                (forall l0 : L,
                                 (xL_plus l0).1 (yR r) <
                                 x_plus_y) *
                                (forall r0 : R,
                                 x_plus_y <
                                 (xR_plus r0).1 (yR r))})
                   (x_plus_yL_lt_yR : forall (l0 : L')
                                      (r : R'),
                                      (x_plus_yL l0).1 <
                                      (x_plus_yR r).1)
                 =>
                 let L'' := L + L' in
                 let R'' := R + R' in
                 let zL :=
                   sum_ind (fun _ : L + L' => No)
                     (fun l0 : L =>
                      (xL_plus l0).1
                        {{ yL | yR//ycut }})
                     (fun l0 : L' => (x_plus_yL l0).1)
                   in
                 let zR :=
                   sum_ind (fun _ : R + R' => No)
                     (fun r : R =>
                      (xR_plus r).1
                        {{ yL | yR//ycut }})
                     (fun r : R' => (x_plus_yR r).1)
                   in
                 let zcut :=
                   plus_inner_subproof L' R' s yL yR
                     ycut x_plus_yL x_plus_yR
                     x_plus_yL_lt_yR in
                 let X := sum_options L R L' R' Sx s
                   in
                 ({{ zL | zR//zcut }};
                 (fun l0 : L =>
                  lt_lopt zL zR zcut (...),
                 fun r : R => lt_ropt zL zR zcut (...))))
                plus_inner_subproof0
                plus_inner_subproof1
                plus_inner_subproof2
                plus_inner_subproof3 (game_of (yL l))
                (isno_game_of (yL l))).1) x))
      (fun x : R + R' =>
       game_of
         (sum_ind (fun _ : R + R' => No)
            (fun r : R =>
             (xR_plus r).1
               {{ fun l : L' =>
                  {|
                    game_of := game_of (yL l);
                    isno_game_of :=
                      isno_game_of (yL l)
                  |} | (fun r0 : R' =>
                        {|
                          game_of := game_of (yR r0);
                          isno_game_of :=
                            isno_game_of (yR r0)
                        |})//ycut }})
            (fun r : R' =>
             (Core.Surreals.No_ind_internal
                (fun y : GenNo S =>
                 {x_plus_y : No &
                 (forall l : L,
                  (xL_plus l).1 y < x_plus_y) *
                 (forall r0 : R,
                  x_plus_y < (xR_plus r0).1 y)})
                (fun (x0 y : GenNo S) (_ : x0 <= y)
                   (z : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 x0 < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 y < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 y)})
                 => z.1 <= w.1)
                (fun (x0 y : GenNo S) (_ : x0 < y)
                   (z : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 x0 < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 y < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 y)})
                 => z.1 < w.1)
                (fun (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)
                   (x_plus_yL : forall l : L',
                                {x_plus_y : No &
                                (forall l0 : L,
                                 (xL_plus l0).1 (yL l) <
                                 x_plus_y) *
                                (forall r0 : R,
                                 x_plus_y <
                                 (xR_plus r0).1 (yL l))})
                   (x_plus_yR : forall r0 : R',
                                {x_plus_y : No &
                                (forall l : L,
                                 (xL_plus l).1 (yR r0) <
                                 x_plus_y) *
                                (forall r1 : R,
                                 x_plus_y <
                                 (xR_plus r1).1
                                   (yR r0))})
                   (x_plus_yL_lt_yR : forall (l : L')
                                      (r0 : R'),
                                      (x_plus_yL l).1 <
                                      (x_plus_yR r0).1)
                 =>
                 let L'' := L + L' in
                 let R'' := R + R' in
                 let zL :=
                   sum_ind (fun _ : L + L' => No)
                     (fun l : L =>
                      (xL_plus l).1
                        {{ yL | yR//ycut }})
                     (fun l : L' => (x_plus_yL l).1)
                   in
                 let zR :=
                   sum_ind (fun _ : R + R' => No)
                     (fun r0 : R =>
                      (xR_plus r0).1
                        {{ yL | yR//ycut }})
                     (fun r0 : R' => (x_plus_yR r0).1)
                   in
                 let zcut :=
                   plus_inner_subproof L' R' s yL yR
                     ycut x_plus_yL x_plus_yR
                     x_plus_yL_lt_yR in
                 let X := sum_options L R L' R' Sx s
                   in
                 ({{ zL | zR//zcut }};
                 (fun l : L =>
                  lt_lopt zL zR zcut (...),
                 fun r0 : R =>
                 lt_ropt zL zR zcut (...))))
                plus_inner_subproof0
                plus_inner_subproof1
                plus_inner_subproof2
                plus_inner_subproof3 (game_of (yR r))
                (isno_game_of (yR r))).1) x))
      (fun x : L + L' =>
       isno_game_of
         (sum_ind (fun _ : L + L' => No)
            (fun l : L =>
             (xL_plus l).1
               {{ fun l0 : L' =>
                  {|
                    game_of := game_of (yL l0);
                    isno_game_of :=
                      isno_game_of (yL l0)
                  |} | (fun r : R' =>
                        {|
                          game_of := game_of (yR r);
                          isno_game_of :=
                            isno_game_of (yR r)
                        |})//ycut }})
            (fun l : L' =>
             (Core.Surreals.No_ind_internal
                (fun y : GenNo S =>
                 {x_plus_y : No &
                 (forall l0 : L,
                  (xL_plus l0).1 y < x_plus_y) *
                 (forall r : R,
                  x_plus_y < (xR_plus r).1 y)})
                (fun (x0 y : GenNo S) (_ : x0 <= y)
                   (z : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 x0 < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 y < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 y)})
                 => z.1 <= w.1)
                (fun (x0 y : GenNo S) (_ : x0 < y)
                   (z : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 x0 < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l0 : L,
                         (xL_plus l0).1 y < x_plus_y) *
                        (forall r : R,
                         x_plus_y < (xR_plus r).1 y)})
                 => z.1 < w.1)
                (fun (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)
                   (x_plus_yL : forall l0 : L',
                                {x_plus_y : No &
                                (forall l1 : L,
                                 (xL_plus l1).1
                                   (yL l0) < x_plus_y) *
                                (forall r : R,
                                 x_plus_y <
                                 (xR_plus r).1 (yL l0))})
                   (x_plus_yR : forall r : R',
                                {x_plus_y : No &
                                (forall l0 : L,
                                 (xL_plus l0).1 (yR r) <
                                 x_plus_y) *
                                (forall r0 : R,
                                 x_plus_y <
                                 (xR_plus r0).1 (yR r))})
                   (x_plus_yL_lt_yR : forall (l0 : L')
                                      (r : R'),
                                      (x_plus_yL l0).1 <
                                      (x_plus_yR r).1)
                 =>
                 let L'' := L + L' in
                 let R'' := R + R' in
                 let zL :=
                   sum_ind (fun _ : L + L' => No)
                     (fun l0 : L =>
                      (xL_plus l0).1
                        {{ yL | yR//ycut }})
                     (fun l0 : L' => (x_plus_yL l0).1)
                   in
                 let zR :=
                   sum_ind (fun _ : R + R' => No)
                     (fun r : R =>
                      (xR_plus r).1
                        {{ yL | yR//ycut }})
                     (fun r : R' => (x_plus_yR r).1)
                   in
                 let zcut :=
                   plus_inner_subproof L' R' s yL yR
                     ycut x_plus_yL x_plus_yR
                     x_plus_yL_lt_yR in
                 let X := sum_options L R L' R' Sx s
                   in
                 ({{ zL | zR//zcut }};
                 (fun l0 : L =>
                  lt_lopt zL zR zcut (...),
                 fun r : R => lt_ropt zL zR zcut (...))))
                plus_inner_subproof0
                plus_inner_subproof1
                plus_inner_subproof2
                plus_inner_subproof3 (game_of (yL l))
                (isno_game_of (yL l))).1) x))
      (fun x : R + R' =>
       isno_game_of
         (sum_ind (fun _ : R + R' => No)
            (fun r : R =>
             (xR_plus r).1
               {{ fun l : L' =>
                  {|
                    game_of := game_of (yL l);
                    isno_game_of :=
                      isno_game_of (yL l)
                  |} | (fun r0 : R' =>
                        {|
                          game_of := game_of (yR r0);
                          isno_game_of :=
                            isno_game_of (yR r0)
                        |})//ycut }})
            (fun r : R' =>
             (Core.Surreals.No_ind_internal
                (fun y : GenNo S =>
                 {x_plus_y : No &
                 (forall l : L,
                  (xL_plus l).1 y < x_plus_y) *
                 (forall r0 : R,
                  x_plus_y < (xR_plus r0).1 y)})
                (fun (x0 y : GenNo S) (_ : x0 <= y)
                   (z : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 x0 < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 y < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 y)})
                 => z.1 <= w.1)
                (fun (x0 y : GenNo S) (_ : x0 < y)
                   (z : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 x0 < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 x0)})
                   (w : {x_plus_y : No &
                        (forall l : L,
                         (xL_plus l).1 y < x_plus_y) *
                        (forall r0 : R,
                         x_plus_y < (xR_plus r0).1 y)})
                 => z.1 < w.1)
                (fun (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)
                   (x_plus_yL : forall l : L',
                                {x_plus_y : No &
                                (forall l0 : L,
                                 (xL_plus l0).1 (yL l) <
                                 x_plus_y) *
                                (forall r0 : R,
                                 x_plus_y <
                                 (xR_plus r0).1 (yL l))})
                   (x_plus_yR : forall r0 : R',
                                {x_plus_y : No &
                                (forall l : L,
                                 (xL_plus l).1 (yR r0) <
                                 x_plus_y) *
                                (forall r1 : R,
                                 x_plus_y <
                                 (xR_plus r1).1
                                   (yR r0))})
                   (x_plus_yL_lt_yR : forall (l : L')
                                      (r0 : R'),
                                      (x_plus_yL l).1 <
                                      (x_plus_yR r0).1)
                 =>
                 let L'' := L + L' in
                 let R'' := R + R' in
                 let zL :=
                   sum_ind (fun _ : L + L' => No)
                     (fun l : L =>
                      (xL_plus l).1
                        {{ yL | yR//ycut }})
                     (fun l : L' => (x_plus_yL l).1)
                   in
                 let zR :=
                   sum_ind (fun _ : R + R' => No)
                     (fun r0 : R =>
                      (xR_plus r0).1
                        {{ yL | yR//ycut }})
                     (fun r0 : R' => (x_plus_yR r0).1)
                   in
                 let zcut :=
                   plus_inner_subproof L' R' s yL yR
                     ycut x_plus_yL x_plus_yR
                     x_plus_yL_lt_yR in
                 let X := sum_options L R L' R' Sx s
                   in
                 ({{ zL | zR//zcut }};
                 (fun l : L =>
                  lt_lopt zL zR zcut (...),
                 fun r0 : R =>
                 lt_ropt zL zR zcut (...))))
                plus_inner_subproof0
                plus_inner_subproof1
                plus_inner_subproof2
                plus_inner_subproof3 (game_of (yR r))
                (isno_game_of (yR r))).1) x))
      (plus_inner_subproof L' R' Sy
         (fun l : L' =>
          {|
            game_of := game_of (yL l);
            isno_game_of := isno_game_of (yL l)
          |})
         (fun r : R' =>
          {|
            game_of := game_of (yR r);
            isno_game_of := isno_game_of (yR r)
          |}) ycut
         (fun l : L' =>
          Core.Surreals.No_ind_internal
            (fun y : GenNo S =>
             {x_plus_y : No &
             (forall l0 : L,
              (xL_plus l0).1 y < x_plus_y) *
             (forall r : R, x_plus_y < (xR_plus r).1 y)})
            (fun (x y : GenNo S) (_ : x <= y)
               (z : {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 x < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 x)})
               (w : {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 y)}) =>
             z.1 <= w.1)
            (fun (x y : GenNo S) (_ : x < y)
               (z : {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 x < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 x)})
               (w : {x_plus_y : No &
                    (forall l0 : L,
                     (xL_plus l0).1 y < x_plus_y) *
                    (forall r : R,
                     x_plus_y < (xR_plus r).1 y)}) =>
             z.1 < w.1)
            (fun (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)
               (x_plus_yL : forall l0 : L',
                            {x_plus_y : No &
                            (forall l1 : L,
                             (xL_plus l1).1 (yL l0) <
                             x_plus_y) *
                            (forall r : R,
                             x_plus_y <
                             (xR_plus r).1 (yL l0))})
               (x_plus_yR : forall r : R',
                            {x_plus_y : No &
                            (forall l0 : L,
                             (xL_plus l0).1 (yR r) <
                             x_plus_y) *
                            (forall r0 : R,
                             x_plus_y <
                             (xR_plus r0).1 (yR r))})
               (x_plus_yL_lt_yR : forall (l0 : L')
                                  (r : R'),
                                  (x_plus_yL l0).1 <
                                  (x_plus_yR r).1) =>
             let L'' := L + L' in
             let R'' := R + R' in
             let zL :=
               sum_ind (fun _ : L + L' => No)
                 (fun l0 : L =>
                  (xL_plus l0).1 {{ yL | yR//ycut }})
                 (fun l0 : L' => (x_plus_yL l0).1) in
             let zR :=
               sum_ind (fun _ : R + R' => No)
                 (fun r : R =>
                  (xR_plus r).1 {{ yL | yR//ycut }})
                 (fun r : R' => (x_plus_yR r).1) in
             let zcut :=
               plus_inner_subproof L' R' s yL yR ycut
                 x_plus_yL x_plus_yR x_plus_yL_lt_yR
               in
             let X := sum_options L R L' R' Sx s in
             ({{ zL | zR//zcut }};
             (fun l0 : L =>
              lt_lopt zL zR zcut (inl l0),
             fun r : R => lt_ropt zL zR zcut (inl r))))
            plus_inner_subproof0 plus_inner_subproof1
            plus_inner_subproof2 plus_inner_subproof3
            (game_of (yL l)) (isno_game_of (yL l)))
         (fun r : R' =>
          Core.Surreals.No_ind_internal
            (fun y : GenNo S =>
             {x_plus_y : No &
             (forall l : L, (xL_plus l).1 y < x_plus_y) *
             (forall r0 : R,
              x_plus_y < (xR_plus r0).1 y)})
            (fun (x y : GenNo S) (_ : x <= y)
               (z : {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 x < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 x)})
               (w : {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)}) =>
             z.1 <= w.1)
            (fun (x y : GenNo S) (_ : x < y)
               (z : {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 x < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 x)})
               (w : {x_plus_y : No &
                    (forall l : L,
                     (xL_plus l).1 y < x_plus_y) *
                    (forall r0 : R,
                     x_plus_y < (xR_plus r0).1 y)}) =>
             z.1 < w.1)
            (fun (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)
               (x_plus_yL : forall l : L',
                            {x_plus_y : No &
                            (forall l0 : L,
                             (xL_plus l0).1 (yL l) <
                             x_plus_y) *
                            (forall r0 : R,
                             x_plus_y <
                             (xR_plus r0).1 (yL l))})
               (x_plus_yR : forall r0 : R',
                            {x_plus_y : No &
                            (forall l : L,
                             (xL_plus l).1 (yR r0) <
                             x_plus_y) *
                            (forall r1 : R,
                             x_plus_y <
                             (xR_plus r1).1 (yR r0))})
               (x_plus_yL_lt_yR : forall (l : L')
                                  (r0 : R'),
                                  (x_plus_yL l).1 <
                                  (x_plus_yR r0).1) =>
             let L'' := L + L' in
             let R'' := R + R' in
             let zL :=
               sum_ind (fun _ : L + L' => No)
                 (fun l : L =>
                  (xL_plus l).1 {{ yL | yR//ycut }})
                 (fun l : L' => (x_plus_yL l).1) in
             let zR :=
               sum_ind (fun _ : R + R' => No)
                 (fun r0 : R =>
                  (xR_plus r0).1 {{ yL | yR//ycut }})
                 (fun r0 : R' => (x_plus_yR r0).1) in
             let zcut :=
               plus_inner_subproof L' R' s yL yR ycut
                 x_plus_yL x_plus_yR x_plus_yL_lt_yR
               in
             let X := sum_options L R L' R' Sx s in
             ({{ zL | zR//zcut }};
             (fun l : L => lt_lopt zL zR zcut (inl l),
             fun r0 : R => lt_ropt zL zR zcut (inl r0))))
            plus_inner_subproof0 plus_inner_subproof1
            plus_inner_subproof2 plus_inner_subproof3
            (game_of (yR r)) (isno_game_of (yR r)))
         (fun (l : L') (r : R') =>
          match
            No_Empty_admitted
            return
              ((Core.Surreals.No_ind_internal
                  (fun y : GenNo S =>
                   {x_plus_y : No &
                   (forall l0 : L,
                    (xL_plus l0).1 y < x_plus_y) *
                   (forall r0 : R,
                    x_plus_y < (xR_plus r0).1 y)})
                  (fun (x y : GenNo S) (_ : x <= y)
                     (z : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 x < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 x)})
                     (w : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 y < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 y)}) =>
                   z.1 <= w.1)
                  (fun (x y : GenNo S) (_ : x < y)
                     (z : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 x < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 x)})
                     (w : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 y < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 y)}) =>
                   z.1 < w.1)
                  (fun (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)
                     (x_plus_yL : forall l0 : L',
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   ... < x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y < ...)})
                     (x_plus_yR : forall r0 : R',
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   ... < x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y < ...)})
                     (x_plus_yL_lt_yR : forall
                                        (l0 : L')
                                        (r0 : R'),
                                        (x_plus_yL l0).1 <
                                        (x_plus_yR r0).1)
                   =>
                   let L'' := L + L' in
                   let R'' := R + R' in
                   let zL :=
                     sum_ind (fun ... => No)
                       (fun ... =>
                        ....1 {{ yL | yR//ycut }})
                       (fun ... => (...).1) in
                   let zR :=
                     sum_ind (... => No) (... => ...)
                       (... => ....1) in
                   let zcut :=
                     plus_inner_subproof L' R' s yL yR
                       ycut x_plus_yL x_plus_yR
                       x_plus_yL_lt_yR in
                   let X := sum_options L R L' R' Sx s
                     in
                   ({{ zL | zR//zcut }}; (..., ...)))
                  plus_inner_subproof0
                  plus_inner_subproof1
                  plus_inner_subproof2
                  plus_inner_subproof3
                  (game_of (yL l))
                  (isno_game_of (yL l))).1 <
               (Core.Surreals.No_ind_internal
                  (fun y : GenNo S =>
                   {x_plus_y : No &
                   (forall l0 : L,
                    (xL_plus l0).1 y < x_plus_y) *
                   (forall r0 : R,
                    x_plus_y < (xR_plus r0).1 y)})
                  (fun (x y : GenNo S) (_ : x <= y)
                     (z : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 x < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 x)})
                     (w : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 y < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 y)}) =>
                   z.1 <= w.1)
                  (fun (x y : GenNo S) (_ : x < y)
                     (z : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 x < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 x)})
                     (w : {x_plus_y : No &
                          (forall l0 : L,
                           ....1 y < x_plus_y) *
                          (forall r0 : R,
                           x_plus_y < ....1 y)}) =>
                   z.1 < w.1)
                  (fun (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)
                     (x_plus_yL : forall l0 : L',
                                  {x_plus_y : No &
                                  (forall l1 : L,
                                   ... < x_plus_y) *
                                  (forall r0 : R,
                                   x_plus_y < ...)})
                     (x_plus_yR : forall r0 : R',
                                  {x_plus_y : No &
                                  (forall l0 : L,
                                   ... < x_plus_y) *
                                  (forall r1 : R,
                                   x_plus_y < ...)})
                     (x_plus_yL_lt_yR : forall
                                        (l0 : L')
                                        (r0 : R'),
                                        (x_plus_yL l0).1 <
                                        (x_plus_yR r0).1)
                   =>
                   let L'' := L + L' in
                   let R'' := R + R' in
                   let zL :=
                     sum_ind (fun ... => No)
                       (fun ... =>
                        ....1 {{ yL | yR//ycut }})
                       (fun ... => (...).1) in
                   let zR :=
                     sum_ind (... => No) (... => ...)
                       (... => ....1) in
                   let zcut :=
                     plus_inner_subproof L' R' s yL yR
                       ycut x_plus_yL x_plus_yR
                       x_plus_yL_lt_yR in
                   let X := sum_options L R L' R' Sx s
                     in
                   ({{ zL | zR//zcut }}; (..., ...)))
                  plus_inner_subproof0
                  plus_inner_subproof1
                  plus_inner_subproof2
                  plus_inner_subproof3
                  (game_of (yR r))
                  (isno_game_of (yR r))).1)
          with
          end))
|} =
{|
  game_of :=
    opt (L + L') (R + R')
      (sum_options L R L' R' Sx Sy)
      (fun x : L + L' =>
       game_of
         (sum_ind (fun _ : L + L' => No)
            (fun l : L =>
             (xL_plus l).1 {{ yL | yR//ycut }})
            (fun l : L' => (plus_inner.1 (yL l)).1) x))
      (fun x : R + R' =>
       game_of
         (sum_ind (fun _ : R + R' => No)
            (fun r : R =>
             (xR_plus r).1 {{ yL | yR//ycut }})
            (fun r : R' => (plus_inner.1 (yR r)).1) x));
  isno_game_of :=
    isno (L + L') (R + R')
      (sum_options L R L' R' Sx Sy)
      (fun x : L + L' =>
       game_of
         (sum_ind (fun _ : L + L' => No)
            (fun l : L =>
             (xL_plus l).1 {{ yL | yR//ycut }})
            (fun l : L' => (plus_inner.1 (yL l)).1) x))
      (fun x : R + R' =>
       game_of
         (sum_ind (fun _ : R + R' => No)
            (fun r : R =>
             (xR_plus r).1 {{ yL | yR//ycut }})
            (fun r : R' => (plus_inner.1 (yR r)).1) x))
      (fun x : L + L' =>
       isno_game_of
         (sum_ind (fun _ : L + L' => No)
            (fun l : L =>
             (xL_plus l).1 {{ yL | yR//ycut }})
            (fun l : L' => (plus_inner.1 (yL l)).1) x))
      (fun x : R + R' =>
       isno_game_of
         (sum_ind (fun _ : R + R' => No)
            (fun r : R =>
             (xR_plus r).1 {{ yL | yR//ycut }})
            (fun r : R' => (plus_inner.1 (yR r)).1) x))
      ?zcut
|} reflexivity.
    Qed.

  End Inner.

  Definition plus_outer
  : { f : No -> { g : No -> No &
                  (forall x y, x <= y -> g x <= g y) *
                  (forall x y, x <  y -> g x <  g y) } &
      (forall x y, x <= y -> forall z, (f x).1 z <= (f y).1 z) *
      (forall x y, x <  y -> forall z, (f x).1 z <  (f y).1 z) }.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
{f
: No ->
  {g : No -> No &
  (forall x y : GenNo S, x <= y -> g x <= g y) *
  (forall x y : GenNo S, x < y -> g x < g y)} &
(forall x y : GenNo S,
 x <= y -> forall z : No, (f x).1 z <= (f y).1 z) *
(forall x y : GenNo S,
 x < y -> forall z : No, (f x).1 z < (f y).1 z)}
  Proof.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
{f
: No ->
  {g : No -> No &
  (forall x y : GenNo S, x <= y -> g x <= g y) *
  (forall x y : GenNo S, x < y -> g x < g y)} &
(forall x y : GenNo S,
 x <= y -> forall z : No, (f x).1 z <= (f y).1 z) *
(forall x y : GenNo S,
 x < y -> forall z : No, (f x).1 z < (f y).1 z)}
    refine (No_rec_package
              {g : No -> No &
                (forall x y, x <= y -> g x <= g y) *
                (forall x y, x <  y -> g x <  g y) }
              (fun g h => forall x, g.1 x <= h.1 x)
              (fun g h => forall x, g.1 x <  h.1 x)
              (fun L R Sx xL xR xcut xL_plus xR_plus xL_lt_xR_plus =>
                 let g := plus_inner xL_plus xR_plus xL_lt_xR_plus in
                 ((fun y => (g.1 y).1) ; (g.2)))
               _ _ _ _).
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall
a
 b : {g : No -> No &
     (forall x y : GenNo S, x <= y -> g x <= g y) *
     (forall x y : GenNo S, x < y -> g x < g y)},
(forall x : No, a.1 x <= b.1 x) ->
(forall x : No, b.1 x <= a.1 x) -> a = b
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall (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 ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxR : R ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxcut : forall (l : L) (r : R) (x : No),
         (fxL l).1 x < (fxR r).1 x) (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' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fyR : R' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fycut : forall (l : L') (r : R') (x : No),
         (fyL l).1 x < (fyR r).1 x),
(forall l : L, xL l < {{ yL | yR//ycut }}) ->
(forall (l : L) (x : No),
 (fxL l).1 x <
 (let g := plus_inner fyL fyR fycut in
  (fun y : No => (g.1 y).1; g.2)).1 x) ->
(forall r : R', {{ xL | xR//xcut }} < yR r) ->
(forall (r : R') (x : No),
 (let g := plus_inner fxL fxR fxcut in
  (fun y : No => (g.1 y).1; g.2)).1 x < (fyR r).1 x) ->
forall x : No,
(let g := plus_inner fxL fxR fxcut in
 (fun y : No => (g.1 y).1; g.2)).1 x <=
(let g := plus_inner fyL fyR fycut in
 (fun y : No => (g.1 y).1; g.2)).1 x
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall (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 ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxR : R ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxcut : forall (l : L) (r : R) (x : No),
         (fxL l).1 x < (fxR r).1 x) (L' R' : Type)
(s' : InSort S L' R') (yL : L' -> GenNo S)
(yR : R' -> GenNo S),
(forall (l : L') (r : R'), yL l < yR r) ->
forall
(fyL : L' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fyR : R' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fycut : forall (l : L') (r : R') (x : No),
         (fyL l).1 x < (fyR r).1 x) (l : L'),
{{ xL | xR//xcut }} <= yL l ->
(forall x : No,
 (let g := plus_inner fxL fxR fxcut in
  (fun y : No => (g.1 y).1; g.2)).1 x <= (fyL l).1 x) ->
forall x : No,
(let g := plus_inner fxL fxR fxcut in
 (fun y : No => (g.1 y).1; g.2)).1 x <
(let g := plus_inner fyL fyR fycut in
 (fun y : No => (g.1 y).1; g.2)).1 x
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall (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) ->
forall
(fxL : L ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxR : R ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxcut : forall (l : L) (r : R) (x : No),
         (fxL l).1 x < (fxR r).1 x) (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' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fyR : R' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fycut : forall (l : L') (r : R') (x : No),
         (fyL l).1 x < (fyR r).1 x) (r : R),
xR r <= {{ yL | yR//ycut }} ->
(forall x : No,
 (fxR r).1 x <=
 (let g := plus_inner fyL fyR fycut in
  (fun y : No => (g.1 y).1; g.2)).1 x) ->
forall x : No,
(let g := plus_inner fxL fxR fxcut in
 (fun y : No => (g.1 y).1; g.2)).1 x <
(let g := plus_inner fyL fyR fycut in
 (fun y : No => (g.1 y).1; g.2)).1 x
    -
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall
a
 b : {g : No -> No &
     (forall x y : GenNo S, x <= y -> g x <= g y) *
     (forall x y : GenNo S, x < y -> g x < g y)},
(forall x : No, a.1 x <= b.1 x) ->
(forall x : No, b.1 x <= a.1 x) -> a = b abstract (
      intros [g ?] [h ?] p q;
      apply path_sigma_hprop; cbn in *;
      apply path_arrow; intros x;
      apply path_No; [ apply p | apply q ] ).
    -
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall (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 ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxR : R ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxcut : forall (l : L) (r : R) (x : No),
         (fxL l).1 x < (fxR r).1 x) (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' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fyR : R' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fycut : forall (l : L') (r : R') (x : No),
         (fyL l).1 x < (fyR r).1 x),
(forall l : L, xL l < {{ yL | yR//ycut }}) ->
(forall (l : L) (x : No),
 (fxL l).1 x <
 (let g := plus_inner fyL fyR fycut in
  (fun y : No => (g.1 y).1; g.2)).1 x) ->
(forall r : R', {{ xL | xR//xcut }} < yR r) ->
(forall (r : R') (x : No),
 (let g := plus_inner fxL fxR fxcut in
  (fun y : No => (g.1 y).1; g.2)).1 x < (fyR r).1 x) ->
forall x : No,
(let g := plus_inner fxL fxR fxcut in
 (fun y : No => (g.1 y).1; g.2)).1 x <=
(let g := plus_inner fyL fyR fycut in
 (fun y : No => (g.1 y).1; g.2)).1 x abstract (
      intros L R ? xL xR xcut xL_plus xR_plus xL_lt_xR_plus
           L' R' ? yL yR ycut yL_plus yR_plus yL_lt_yR_plus;
      intros xL_lt_y xL_lt_y_plus x_lt_yR x_lt_yR_plus z;
      lazy beta zeta in *; cbn [pr1] in *;
      pattern z; refine (No_ind_hprop _ _ z);
      intros L'' R'' ? zL zR zcut x_le_y_plus_zL x_le_y_plus_zR;
      destruct (plus_inner_cut xL_plus xR_plus xL_lt_xR_plus
                               zL zR zcut) as [xzcut p]; rewrite p;
      destruct (plus_inner_cut yL_plus yR_plus yL_lt_yR_plus
                               zL zR zcut) as [yzcut q];rewrite q;
      apply le_lr; [ intros [l|l] | intros [r|r] ];
      [ (** x^L + z < y + z *)
        specialize (xL_lt_y_plus l {{ zL | zR // zcut }});
        rewrite q in xL_lt_y_plus;
        exact xL_lt_y_plus
      | (** x + z^L < y + z *)
        refine (le_lt_trans (x_le_y_plus_zL l) _);
        exact (lt_lopt _ _ _ (inr l))
      | (** x + z < y^R + z *)
        specialize (x_lt_yR_plus r {{ zL | zR // zcut }});
        rewrite p in x_lt_yR_plus;
        exact x_lt_yR_plus
      | (** x + z < y + z^R *)
        refine (lt_le_trans _ (x_le_y_plus_zR r));
        exact (lt_ropt _ _ _ (inr r)) ]).
    -
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall (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 ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxR : R ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxcut : forall (l : L) (r : R) (x : No),
         (fxL l).1 x < (fxR r).1 x) (L' R' : Type)
(s' : InSort S L' R') (yL : L' -> GenNo S)
(yR : R' -> GenNo S),
(forall (l : L') (r : R'), yL l < yR r) ->
forall
(fyL : L' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fyR : R' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fycut : forall (l : L') (r : R') (x : No),
         (fyL l).1 x < (fyR r).1 x) (l : L'),
{{ xL | xR//xcut }} <= yL l ->
(forall x : No,
 (let g := plus_inner fxL fxR fxcut in
  (fun y : No => (g.1 y).1; g.2)).1 x <= (fyL l).1 x) ->
forall x : No,
(let g := plus_inner fxL fxR fxcut in
 (fun y : No => (g.1 y).1; g.2)).1 x <
(let g := plus_inner fyL fyR fycut in
 (fun y : No => (g.1 y).1; g.2)).1 x abstract (
      intros L R ? xL xR xcut xL_plus xR_plus xL_lt_xR_plus
             L' R' ? yL yR ycut yL_plus yR_plus yL_lt_yR_plus;
      intros l x_le_yL x_le_yL_plus z;
      lazy beta zeta in *; cbn [pr1] in *;
      pattern z; refine (No_ind_hprop _ _ z);
      intros L'' R'' ? zL zR zcut x_le_y_plus_zL x_le_y_plus_zR;
      destruct (plus_inner_cut xL_plus xR_plus xL_lt_xR_plus
                               zL zR zcut) as [xzcut p]; rewrite p;
      destruct (plus_inner_cut yL_plus yR_plus yL_lt_yR_plus
                               zL zR zcut) as [yzcut q];rewrite q;
      refine (le_lt_trans (x_le_yL_plus {{ zL | zR // zcut }}) _);
      exact (lt_lopt _ _ _ (inl l)) ).
    -
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
forall (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) ->
forall
(fxL : L ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxR : R ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fxcut : forall (l : L) (r : R) (x : No),
         (fxL l).1 x < (fxR r).1 x) (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' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fyR : R' ->
       {g : No -> No &
       (forall x y : GenNo S, x <= y -> g x <= g y) *
       (forall x y : GenNo S, x < y -> g x < g y)})
(fycut : forall (l : L') (r : R') (x : No),
         (fyL l).1 x < (fyR r).1 x) (r : R),
xR r <= {{ yL | yR//ycut }} ->
(forall x : No,
 (fxR r).1 x <=
 (let g := plus_inner fyL fyR fycut in
  (fun y : No => (g.1 y).1; g.2)).1 x) ->
forall x : No,
(let g := plus_inner fxL fxR fxcut in
 (fun y : No => (g.1 y).1; g.2)).1 x <
(let g := plus_inner fyL fyR fycut in
 (fun y : No => (g.1 y).1; g.2)).1 x abstract (
      intros L R ? xL xR xcut xL_plus xR_plus xL_lt_xR_plus
             L' R' ? yL yR ycut yL_plus yR_plus yL_lt_yR_plus;
      intros r xR_le_y xR_le_y_plus z;
      lazy beta zeta in *; cbn [pr1] in *;
      pattern z; refine (No_ind_hprop _ _ z);
      intros L'' R'' ? zL zR zcut x_le_y_plus_zL x_le_y_plus_zR;
      destruct (plus_inner_cut xL_plus xR_plus xL_lt_xR_plus
                               zL zR zcut) as [xzcut p]; rewrite p;
      destruct (plus_inner_cut yL_plus yR_plus yL_lt_yR_plus
                               zL zR zcut) as [yzcut q];rewrite q;
      refine (lt_le_trans _ (xR_le_y_plus {{ zL | zR // zcut }}));
      exact (lt_ropt _ _ _ (inl r)) ).
  Defined.

  Definition plus (x y : No) : No
    := (plus_outer.1 x).1 y.

  Infix "+" := plus : surreal_scope.

  Definition plus_le_l (x x' y : No) (p : x <= x')
  : (x + y) <= (x' + y)
    := fst (plus_outer.2) x x' p y.

  Definition plus_lt_l (x x' y : No) (p : x < x')
  : (x + y) < (x' + y)
    := snd (plus_outer.2) x x' p y.

  Definition plus_le_r (x y y' : No) (p : y <= y')
  : (x + y) <= (x + y')
    := fst (plus_outer.1 x).2 y y' p.

  Definition plus_lt_r (x y y' : No) (p : y < y')
  : (x + y) < (x + y')
    := snd (plus_outer.1 x).2 y y' p.

  (** See the remarks above [plus_inner_cut] to explain the type of this lemma. *)
  Definition plus_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)
             {L' R' : Type@{i} } {Sy : InSort S L' R'}
             (yL : L' -> No) (yR : R' -> No)
             (ycut : forall (l : L') (r : R'), yL l < yR r)
  : let L'' := (L + L')%type in
    let R'' := (R + R')%type in
    let x := {{ xL | xR // xcut }} in
    let y := {{ yL | yR // ycut }} in
    let zL := sum_ind (fun _ => No)
                      (fun l => (xL l) + y) (fun l => x + (yL l))
              : L'' -> No in
    let zR := sum_ind (fun _ => No)
                      (fun r => (xR r) + y) (fun r => x + (yR r))
              : R'' -> No in
    let Sz := sum_options L R L' R' _ _ in
    { zcut : forall (l:L'') (r:R''), zL l < zR r &
      x + y = @No_cut _ _ _ Sz zL zR zcut }
    := plus_inner_cut (Sx := Sx)
         (fun l => plus_outer.1 (xL l))
         (fun r => plus_outer.1 (xR r))
         (fun l r => snd plus_outer.2 (xL l) (xR r) (xcut l r))
         yL yR ycut.

  (** Because the conclusion of [plus_cut] is a sigma-type whose second component is the real equality we want to rewrite along, in order to rewrite along it we have to first destruct it.  This tactic takes care of that for us. *)
  Ltac do_plus_cut :=
    repeat match goal with
    | [ |- context ctx [ {{ ?xL | ?xR // ?xcut }} + {{ ?yL | ?yR // ?ycut }} ] ] =>
      let xycut := fresh "cut" in
      let p := fresh "p" in
      destruct (plus_cut xL xR xcut yL yR ycut) as [xycut p];
        rewrite p; clear p
    end.

  (** Conway proves the basic properties of arithmetic using "one-line proofs".  We can't quite do them in one line of Ltac, but the following tactic does help a lot.  Note that it is specific to addition.  It requires the caller to specify the equivalences along which to identify the indexing types for the options, as well as a rewriting tactic for evaluating those equivalences on constructors.  Unfortunately, it doesn't usually manage to finish the whole proof, since in general it can't guess how to use the inductive hypotheses.  It's usually fairly easy to finish all the cases it leaves over, but we do generally have to refer by name to the inductive hypotheses that were automatically named by [intros] here.  I haven't thought of a good solution to that. *)
  Local Opaque No_cut plus. (* required to make [rewrite] fail quickly *)
  Local Unset Keyed Unification. (* shaves another second or two off of [rewrite] *)
  Tactic Notation "one_line_proof" uconstr(eL) uconstr(eR) :=
    unfold No in *;
    repeat_No_ind_hprop;
    do_plus_cut;
    refine (path_No_easy _ _ _ _ eL eR _ _ _ _);
    intros;
    repeat match goal with
           | [ H : (?A + ?B) |- _ ] => destruct H
           end;
    repeat match goal with
           | [ |- context[@equiv_fun ?A ?B ?e ?v] ]
             => (* first check that we picked up either [eL] or [eR]; we can't use [unify] because it doesn't infer holes, and we can't Ltac-match on [eL] / [eR] because apparently matching on uconstr doesn't work when there are holes in the uconstr *)
             first [ let unif := constr:(idpath : e = eL) in idtac
                   | let unif := constr:(idpath : e = eR) in idtac ];
             (* assume that the term reduces to a constructor; use [hnf] to get that constructor *)
             let ef := constr:(@equiv_fun A B e v) in
             let ef' := (eval hnf in ef) in
             progress change ef with ef'
           end;
    repeat cbn [sum_ind];
    (* rewrite with induction hypotheses from [repeat_No_ind_hprop] and [do_plus_cut] *)
    repeat match goal with
           | [ |- ?x = ?x ] => reflexivity
           | [ |- ?a + _ = ?a + _ ] => apply ap
           | [ |- _ + ?a = _ + ?a ] => apply (ap (fun x => x + a))
           | [ e : Empty |- _ ] => elim e
           | [ IH : (forall lr, _ + _ = _) |- _ ]
             => rewrite IH; clear IH
           | [ IH : (forall lr, _ + _ = _ + _) |- _ ]
             => first [ rewrite IH | rewrite <- IH ]; clear IH
           | [ IH : (forall lr (y : GenNo _), _ + _ = _ + _) |- _ ]
             => first [ rewrite IH | rewrite <- IH ]; clear IH
           | [ IH : (forall lr (y z : GenNo _), _ + _ = _ + _) |- _ ]
             => first [ rewrite IH | rewrite <- IH ]; clear IH
           end.

  (** At last we are ready to prove that the surreal numbers are a commutative monoid under addition. *)

  Theorem plus_comm (x y : No) : x + y = y + x.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x, y: No
x + y = y + x
  Proof.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x, y: No
x + y = y + x
    one_line_proof (equiv_sum_symm _ _) (equiv_sum_symm _ _).
  Defined.

  Theorem plus_assoc (x y z : No) : (x + y) + z = x + (y + z).
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x, y, z: No
x + y + z = x + (y + z)
  Proof.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x, y, z: No
x + y + z = x + (y + z)
    one_line_proof (equiv_sum_assoc _ _ _) (equiv_sum_assoc _ _ _);
      one_line_proof 1%equiv 1%equiv.
  Defined.

  Theorem plus_zero (x : No) : x + zero = x.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x: No
x + zero = x
  Proof.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x: No
x + zero = x
    unfold zero.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x: No
x + {{ Empty_rec | Empty_rec//lempty_cut }} = x
    one_line_proof (sum_empty_r _) (sum_empty_r _).
  Defined.

  Theorem zero_plus (x : No) : zero + x = x.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x: No
zero + x = x
  Proof.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x: No
zero + x = x
    unfold zero.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
x: No
{{ Empty_rec | Empty_rec//lempty_cut }} + x = x
    one_line_proof (sum_empty_l _) (sum_empty_l _).
  Defined.

  (** If we also have negation, we can prove that it gives additive inverses, so that we have an abelian group. *)
  Context `{HasNegation S}.

  Definition plus_negate (x : No) : x + negate x = zero.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
x: No
x + negate x = zero
  Proof.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
x: No
x + negate x = zero
    unfold No in *;
    repeat_No_ind_hprop;
    destruct (negate_cut xL xR xcut) as [nxcut p];
    rewrite p; clear p;
    do_plus_cut.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
{{ sum_ind (fun _ : L + R => No)
     (fun l : L =>
      xL l +
      {{ fun r : R => negate (xR r) | (fun l0 : L =>
                                       negate (xL l0))//nxcut }})
     (fun l : R => {{ xL | xR//xcut }} + negate (xR l)) | 
sum_ind (fun _ : R + L => No)
  (fun r : R =>
   xR r +
   {{ fun r0 : R => negate (xR r0) | (fun l : L =>
                                      negate (xL l))//nxcut }})
  (fun r : L => {{ xL | xR//xcut }} + negate (xL r))//cut }} =
zero
    apply path_No.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
{{ sum_ind (fun _ : L + R => No)
     (fun l : L =>
      xL l +
      {{ fun r : R => negate (xR r) | (fun l0 : L =>
                                       negate (xL l0))//nxcut }})
     (fun l : R => {{ xL | xR//xcut }} + negate (xR l)) | 
sum_ind (fun _ : R + L => No)
  (fun r : R =>
   xR r +
   {{ fun r0 : R => negate (xR r0) | (fun l : L =>
                                      negate (xL l))//nxcut }})
  (fun r : L => {{ xL | xR//xcut }} + negate (xL r))//cut }} <=
zero
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
zero <=
{{ sum_ind (fun _ : L + R => No)
     (fun l : L =>
      xL l +
      {{ fun r : R => negate (xR r) | 
      (fun l0 : L => negate (xL l0))//nxcut }})
     (fun l : R => {{ xL | xR//xcut }} + negate (xR l)) | 
sum_ind (fun _ : R + L => No)
  (fun r : R =>
   xR r +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l : L => negate (xL l))//nxcut }})
  (fun r : L => {{ xL | xR//xcut }} + negate (xL r))//cut }}
    -
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
{{ sum_ind (fun _ : L + R => No)
     (fun l : L =>
      xL l +
      {{ fun r : R => negate (xR r) | (fun l0 : L =>
                                       negate (xL l0))//nxcut }})
     (fun l : R => {{ xL | xR//xcut }} + negate (xR l)) | 
sum_ind (fun _ : R + L => No)
  (fun r : R =>
   xR r +
   {{ fun r0 : R => negate (xR r0) | (fun l : L =>
                                      negate (xL l))//nxcut }})
  (fun r : L => {{ xL | xR//xcut }} + negate (xL r))//cut }} <=
zero apply le_lr; [ intros [l|r]; cbn [sum_ind] | intros [] ].
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
xL l +
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }} <
{{ Empty_rec | Empty_rec//lempty_cut }}
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
{{ xL | xR//xcut }} + negate (xR r) <
{{ Empty_rec | Empty_rec//lempty_cut }}
      +
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
xL l +
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }} <
{{ Empty_rec | Empty_rec//lempty_cut }} unfold zero in IHL; rewrite <- (IHL l); clear IHL.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
xL l +
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }} <
xL l + negate (xL l)
        apply plus_lt_r.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }} <
negate (xL l)
        exact (lt_ropt _ _ _ l).
      +
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
{{ xL | xR//xcut }} + negate (xR r) <
{{ Empty_rec | Empty_rec//lempty_cut }} unfold zero in IHR; rewrite <- (IHR r); clear IHR.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
{{ xL | xR//xcut }} + negate (xR r) <
xR r + negate (xR r)
        apply plus_lt_l.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
{{ xL | xR//xcut }} < xR r
        exact (lt_ropt _ _ _ r).
    -
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
zero <=
{{ sum_ind (fun _ : L + R => No)
     (fun l : L =>
      xL l +
      {{ fun r : R => negate (xR r) | (fun l0 : L =>
                                       negate (xL l0))//nxcut }})
     (fun l : R => {{ xL | xR//xcut }} + negate (xR l)) | 
sum_ind (fun _ : R + L => No)
  (fun r : R =>
   xR r +
   {{ fun r0 : R => negate (xR r0) | (fun l : L =>
                                      negate (xL l))//nxcut }})
  (fun r : L => {{ xL | xR//xcut }} + negate (xL r))//cut }} apply le_lr; [ intros [] | intros [r|l] ]; cbn [sum_ind].
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
{{ Empty_rec | Empty_rec//lempty_cut }} <
xR r +
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }}
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
{{ Empty_rec | Empty_rec//lempty_cut }} <
{{ xL | xR//xcut }} + negate (xL l)
      +
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
{{ Empty_rec | Empty_rec//lempty_cut }} <
xR r +
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }} unfold zero in IHR; rewrite <- (IHR r); clear IHR.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
xR r + negate (xR r) <
xR r +
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }}
        apply plus_lt_r.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
r: R
negate (xR r) <
{{ fun r : R => negate (xR r) | (fun l : L =>
                                 negate (xL l))//nxcut }}
        exact (lt_lopt _ _ _ r).
      +
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHL: forall l : L, xL l + negate (xL l) = zero
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
{{ Empty_rec | Empty_rec//lempty_cut }} <
{{ xL | xR//xcut }} + negate (xL l) unfold zero in IHL; rewrite <- (IHL l); clear IHL.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
xL l + negate (xL l) <
{{ xL | xR//xcut }} + negate (xL l)
        apply plus_lt_l.
H: Univalence
S: OptionSort
H0: HasAddition S
No:= GenNo S: Type
H1: HasNegation S
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
IHR: forall r : R, xR r + negate (xR r) = zero
nxcut: forall (r : R) (l : L),
negate (xR r) < negate (xL l)
cut: forall (l : L + R) (r : R + L),
sum_ind (fun _ : L + R => No)
  (fun l0 : L =>
   xL l0 +
   {{ fun r0 : R => negate (xR r0) | 
   (fun l1 : L => negate (xL l1))//nxcut }})
  (fun l0 : R =>
   {{ xL | xR//xcut }} + negate (xR l0)) l <
sum_ind (fun _ : R + L => No)
  (fun r0 : R =>
   xR r0 +
   {{ fun r1 : R => negate (xR r1) | 
   (fun l0 : L => negate (xL l0))//nxcut }})
  (fun r0 : L =>
   {{ xL | xR//xcut }} + negate (xL r0)) r
l: L
xL l < {{ xL | xR//xcut }}
        exact (lt_lopt _ _ _ l).
  Defined.

  Definition sub (x y : No) : No := x + (negate y).

  Infix "-" := sub : surreal_scope.

End Addition.