proposition: Lemma ord_ptypeL_prop a: ord_ptypeL a -> limit_ordinal a /\ omega0 <=o a.
proof: Proof. move=> H; suff h: limit_ordinal a by split; [exact | exact: (limit_ge_omega h)]. move:H => [p op ->];apply:indecomp_limit2; (apply:oopow_pos op). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)