proposition: Lemma Schutte_Cr_p7 a a' b: a <=o a' -> ordinalp b -> Schutte_Cr a' b -> Schutte_Cr a b.
proof: Proof. move => aa ob pa. case: (equal_or_not a a') => h; first by rewrite h. move: pa => [x ox ->]; exists (Sphi a' x) => //. apply: (OS_Sphi (proj32 aa) ox). by symmetry; apply:Sphi_p3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)