fact: Definition scattered_rel r x y := (gle r x y /\ scattered (induced_order r (interval_cc r x y))) \/ (gle r y x /\ scattered (induced_order r (interval_cc r y x))).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)