proposition: Lemma Conway_theorem0_lemma2 `{Funext} (x : No) (xle : x <= x) {L' R' : Type@{i}} {s' : InSort S L' R'} (yL : L' -> No) (yR : R' -> No) (ycut : forall (l:L') (r:R'), (yL l) < (yR r)) (r : R') (p : x = yR r) : {{ yL | yR // ycut }} < x.
proof: Proof. generalize dependent x; refine (No_ind_hprop _ _); intros. apply lt_r with r. exact (transport (fun z => z <= {{ xL | xR // xcut}}) p xle). Defined.
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core