proposition: Lemma ord_ptypeI_prop a: ord_ptypeI a -> osuccp a /\ omega0 <=o a.
proof: Proof. move => [p op ->]; split. exists (omega0 ^o p) => //. apply: (OS_pow OS_omega (proj32_1 op)). move:op => /oge1P /opow_Mo_le;rewrite oopow1 => op. apply: (oleT op (oleS (proj32 op))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)