proposition: Lemma cofinality0: \cf \0o = \0o.
proof: Proof. move: (cofinality_rw OS0) => [_ [f [[ff sf tf] _]] _]. rewrite - sf; apply /set0_P => y ysf. by move: (Vf_target ff ysf); rewrite tf /ord_zero => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)