fact: Definition eta_like0 r (E:=substrate r) := [/\ total_order r, countable_set E, (forall x, inc x E -> exists y, glt r y x), (forall x, inc x E -> exists y, glt r x y) & (forall x y, glt r x y -> exists z, glt r x z /\ glt r z y)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)