proposition: Lemma cofinality_n0 x: ordinalp x -> x <> \0o -> \cf x <> \0o.
proof: Proof. move => ox xnz;move: (cofinality_rw ox) => [p1 [f [[ff sf tf] fp]] _] se. case: xnz; apply /set0_P => y yx. move: (fp _ yx) => [z]; rewrite se; case; case; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)