proposition: Lemma odegree_psi a b: ordinalp a -> ordinalp b -> oopow (odegree (Spsi a b)) = (Spsi a b).
proof: Proof. move => oa ob. have: indecomposable (Spsi a b). rewrite /Spsi; Ytac h; apply:Schutte_Cr_p8'; fprops. by move/indecomp_prop3 => [y oy ->]; rewrite(odegree_opow oy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)