fact: Definition subitv i1 i2 := let: Interval b1l b1r := i1 in let: Interval b2l b2r := i2 in (b2l <= b1l) && (b1r <= b2r).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)