proposition: Lemma ord_ptypeF_prop a: ord_ptypeF a -> osuccp a /\ a <o omega0.
proof: Proof. move=>[aN ag1 _]; split; last by apply /olt_omegaP. move:(cpred_pr aN (nesym (proj2 (clt_ltT clt_01 ag1)))) =>[bN bv]. exists (cpred a); [ exact:(OS_nat bN) | by rewrite - (succ_of_nat bN)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)