fact: Definition semi_open_interval r x := exists a b, [/\ inc a (substrate r), inc b (substrate r), gle r a b & (x = interval_oc r a b \/ x = interval_co r a b)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)