proposition: Lemma nsv_n0 a: ordinalp a -> S a \0o = a.
proof: Proof. move: a; apply: least_ordinal2' => a oa ap. rewrite (nsv_rec oa OS0). suff : doubleI_rg S a \0o = a by move ->; apply:osups_ordinal. set_extens t. case/doubleI_rgP; first by move => [y /in_set0]. by move => [y ya ->]; rewrite (ap _ ya). by move => ta1; apply/doubleI_rgP; right; ex_tac;rewrite (ap _ ta1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)