proposition: Lemma eta_like_pr1 r: eta_like0 r -> substrate r = emptyset \/ cardinal (substrate r) = aleph0.
proof: Proof. move => [ha hb hc hd he]. case: (emptyset_dichot (substrate r)) => hf; [by left | right]. case:(countable_finite_or_N hb) => hg. move: (finite_set_torder_greatest ha hg hf) => [x [ /hd [y yp yq]]]. have /yq ysr: inc y (substrate r) by order_tac. case: (not_le_gt (proj1 ha) ysr yp). by rewrite hg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)