proposition: Lemma Gamma0_p : Sphi Gamma_0 \0o = Gamma_0 /\ forall x, ordinalp x -> Sphi x \0o = x -> Gamma_0 <=o x.
proof: Proof. move: (normal_ofs_fix Sphi_p5 OS0); rewrite -/Gamma_0. by move => [sa sb sc]; split => // x ox; apply: sc; apply:ole0x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)