proposition: Lemma CNF_psi_exists x: ordinalp x -> exists p n, [/\ natp n, CNF_psi_ax p n & x = CNF_psiv p n].
proof: Proof. move => ox; move:(CNFr_exists ox) => [f [n [nN [ax1 ax2] xv]]]. pose g i := inv_psi_omega (f i). have ha:forall i, i <c n -> ordinal_pair (g i). move => i lin; move:(inv_psi_omega_p (ax1 i lin)). by move => [ha /proj31 hb /proj31_1 hc]. have ax:CNF_psi_ax g n. split; [exact | move => i iN lin]. have lin':=(cle_ltT (cleS iN) lin). move: (ax2 _ iN lin) => sa. move:(inv_psi_omega_p (proj31 sa)) => [_ _ _ ->]. move:(inv_psi_omega_p (proj32 sa)) => [_ _ _ ->]. by apply:opow_Mo_le. exists g, n; split; [ exact | exact |]. rewrite xv;apply: (osumf_exten nN) => i lin. rewrite /CNF_from_psi; move:(inv_psi_omega_p (ax1 _ lin)) => [_ _ _ ->]. by rewrite (odegree_opow (ax1 _ lin)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)