proposition: Lemma inv_psi_omega_p2 x (z:= oopow x) (y:= inv_psi_omega x) : ordinalp x ->x <o Gamma_0 -> [/\ pairp y, (P y) <o z, (Q y) <o z & Spsi (P y) (Q y) = z].
proof: Proof. move => pa pb; move:(inv_psi_omega_p pa). rewrite -/z -/y; move => [sa sb sc sd]; split => //. have zg: z <o Gamma_0 by rewrite - Gamma0_epsilon /z; apply:opow_Mo_lt. rewrite - sd;apply:(Spsi_p6 (ole_ltT sb zg) (olt_ltT sc zg)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)