proposition: Lemma osucc_pr0 x (z:= osucc x): ordinalp x -> x <o z /\ (forall w, x <o w -> z <=o w).
proof: Proof. move=> ox; move: (OS_succ ox)=> oz. split; first by apply/(oltP oz); fprops. move=> w /oltP0 [_ ow xw]. split => // t /setU1_P []; last by move=> ->. by apply: (ordinal_transitive ow). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)