proposition: Lemma Os_ordinal x: ordinalp x -> ordinal_set x.
proof: Proof. move=> ox. set t:= union (Zo(\Po x) (fun y=> transitive_set y /\ ordinal_set y)). have tp: ordinal_set t by move => z /setU_P [v zv /Zo_hi [_]]; apply. have ot: ordinalp t. by apply: ordinal_pr=> //;apply: transitive_setU; move=> t' /Zo_hi [pb _]. case: (ordinal_inA ox ot); last by move => ->. move=> /setU_P [v xv /Zop_S aux]. case: (ordinal_irreflexive ox (aux _ xv)). move => tx. case: (ordinal_irreflexive ot). apply: (@setU_i _ (t +s1 t)); [fprops | apply: Zop_i ]. by apply:setU1_sub => //; apply: (ordinal_transitive ox). split; first by apply: (ordinal_transitive (OS_succ ot)). by move=> u /setU1_P; case; [ apply: tp |move=> ->// ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)