proposition: Lemma OS_nsv a b: ordinalp a -> ordinalp b -> ordinalp (S a b).
proof: Proof. move => oa; move: a oa b. apply:least_ordinal2' => a oa ap. apply:least_ordinal2' =>b ob bp. rewrite (nsv_rec oa ob); apply:OS_sups => t /doubleI_rgP; case. by move => [y yb ->]; apply: bp. by move => [y ya ->]; apply: ap. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)