proposition: Lemma nsv_le_prop z a b: ordinalp a -> ordinalp b -> ordinalp z -> (forall x, x <o a -> S x b <o z) -> (forall x, x <o b -> S a x <o z) -> S a b <=o z.
proof: Proof. move => oa ob oz ha hb. rewrite (nsv_rec oa ob). apply:(osups_least oz) => y /doubleI_rgP; case; move => [t ti ->]. by apply: hb; apply/oltP. by apply: ha; apply/oltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)