proposition: Lemma nsv_ge_sum a b: ordinalp a -> ordinalp b -> a +o b <=o (S a b).
proof: Proof. move => oa; move:b; apply: least_ordinal2' => b ob bp. case:(ordinal_limA ob). - move => ->; rewrite (osum0r oa) (nsv_n0 oa); fprops. - move => [c oc cv]; rewrite cv - (osum2_succ oa oc) (nsv_nS oa oc). by apply/oleSSP; apply: bp; rewrite cv; fprops. - move => lb. rewrite (proj2 (osum_normal oa) b lb). apply: (ord_ub_sup (OS_nsv oa ob)). move => c /funI_P [z zb1 ->]; move/(oltP ob): (zb1) => /proj1 le1. exact:(oleT (bp _ zb1) (nsv_ler oa le1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)