fact: Definition scattered_aux1 r x y := (forall u, sub u (interval_cc r x y) -> ((forall a b, inc a u -> inc b u -> a = b) \/ (exists a b, [/\ inc a u, inc b u, glt r a b & (forall z, inc z u -> gle r z a \/ gle r b z)]))).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)