proposition: Lemma Schutte_Cr_p8 a b: ordinalp a -> ordinalp b -> Schutte_Cr a b -> indecomposable b.
proof: Proof. move => oa ob h. have ap:= ole0x oa. by move: (Schutte_Cr_p7 ap ob h); move /(Schutte_Cr_p3 ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)