proposition: Lemma Schutte_Cr_p3 b: ordinalp b -> (Schutte_Cr \0o b <-> indecomposable b).
proof: Proof. move => ob; split. by move => [x ox ->]; rewrite (Sphi_p0 ox); apply:indecomp_prop4. move /indecomp_prop3 => [y oy ->]; rewrite - (Sphi_p0 oy). by exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)