fact: Definition miditv (R : numDomainType) (i : interval R) : R := match i with | Interval (BSide _ a) (BSide _ b) => (a + b) / 2%:R | Interval -oo%O (BSide _ b) => b - 1 | Interval (BSide _ a) +oo%O => a + 1 | Interval -oo%O +oo%O => 0 | _ => 0 end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)