proposition: Lemma OS_succ x: ordinalp x -> ordinalp (osucc x).
proof: Proof. move=> ox y ytx tsy yntxx. case: (equal_or_not y x) => yx; first by rewrite yx; fprops. apply: setU1_r; apply:(ox _ _ tsy yx) => t ty. case /setU1_P: (ytx _ ty) => // tx; rewrite tx in ty. by case: yntxx; apply: (extensionality ytx); apply: setU1_sub => //; apply: tsy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)