proposition: Lemma nsv_nat a b: ordinalp a -> b <o omega0 -> S a b = a +o b.
proof: Proof. move => oa /(oltP OS_omega) bN; move: b bN a oa ; apply:Nat_induction. by move => a oa; rewrite (nsv_n0 oa) (osum0r oa). move => n nN Hr a oa. rewrite (succ_of_nat nN) (nsv_nS oa (OS_nat nN)) (Hr _ oa). by rewrite (osum2_succ oa (OS_nat nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)