proposition: Lemma ordinal_trans_dec x: ordinalp x -> trans_dec_set x.
proof: Proof. move=> ox. set y := Zo (\Po x) trans_dec_set. set t := union y. have: trans_dec_set t by apply: trans_dec_setU=> z /Zo_hi. case: (equal_or_not t x); first by move=> ->. move=> ntx tct; move: (trans_dec_succ tct) => tcst. have stx: sub t x by apply: setU_s2 =>z /Zop_S. have itx:= (ox _ stx (proj1 tct) ntx). case: ((proj2 tcst) _ (succ_i t)). by apply: (setU_i (succ_i t)); apply: Zop_i => //; apply: setU1_sub. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)