proposition: Lemma finite_zero: finite_o \0o.
proof: Proof. split; first by apply: OS0. move=> /EqS /card_eqP; rewrite cardinal_set0 osucc_zero. move => /card_nonempty; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)