proposition: Lemma ordinal0_pr2 r: worder r -> ordinal r = \0o -> substrate r = emptyset.
proof: Proof. move=> /ordinal_o_is ha hb. move: ha; rewrite hb => [] [f [_ _ [bf sf tf] _]]. rewrite (ordinal_o_sr \0o) /ord_zero in tf; rewrite - sf. apply /set0_P => y ysf; empty_tac1 (Vf f y); Wtac; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)