{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.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.