proposition: Theorem lt_ropt `{Funext} {L R : Type@{i}} {s : InSort S L R} (xL : L -> No) (xR : R -> No) (xcut : forall (l:L) (r:R), (xL l) < (xR r)) (r : R) : {{ xL | xR // xcut }} < xR r.
proof: Proof. refine (Conway_theorem0_lemma2 (xR r) _ _ _ _ _ 1). apply le_reflexive. Defined.
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core