proposition: Lemma OS_T1toB x : ordinalp (T1toB x).
proof: Proof. elim:x; first by apply:OS0. move => a oa n b; apply:OS_sum2. apply:(OS_prod2 (OS_pow OS_omega oa) (@OS_succN n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)