{L R : Type@{i} } {Sx : InSort S L R} (xL : L -> No) (xR : R -> No) (xcut : forall (l : L) (r : R), xL l < xR r) : { nxcut : forall r l, negate (xR r) < negate (xL l) & negate {{ xL | xR // xcut }} = {{ (fun r => negate (xR r)) | (fun l => negate (xL l)) // nxcut }} }. Proof. eexists. unfold negate at 1; rewrite No_rec_cut. reflexivity. Defined.
Require Import HoTT.Basics. Require Import HoTT.Spaces.No.Core.