proposition: Lemma nsv_lt_prop z a b: ordinalp a -> ordinalp b -> z <o S a b -> (exists2 x, x <o a & z <=o S x b) \/ (exists2 x, x <o b & z <=o S a x).
proof: Proof. move => oa ob; rewrite (nsv_rec oa ob); set E := doubleI_rg _ _ _ => lt. have oz := (proj31_1 lt). case: (p_or_not_p (exists2 x, inc x E & z <=o x)); last first. move => h. have oE: ordinal_set E. move=> t /setU2_P; case => /funI_P [u ux ->]; apply:OS_nsv => //. apply: (Os_ordinal oa ux). apply: (Os_ordinal ob ux). have zmax: (forall x, inc x E -> x <o z). move => x xE; case: (oleT_el oz (oE _ xE)) => // lezx; case:h; ex_tac. case:(oleNgt (osups_least oz zmax) lt). move => [x /setU2_P xE le]; case: xE => /funI_P [u ux uv]. left; exists u; [ by apply/(oltP oa) | ue]. right; exists u; [ by apply/(oltP ob) | ue]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)