proposition: Lemma maximal_critical_p1 x: indecomposable x -> exists2 a, ordinalp a & maximal_critical a x.
proof: Proof. move => ix; move: (Sphi_p10b ix) => [a [b [pa pb pc]]]. have oa:=proj31 pa. by exists a => //; apply/(maximal_criticalP oa (proj32 pa)); exists b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)