fact: Definition add_itv_subdef (i1 i2 : interval int) : interval int := let 'Interval l1 u1 := i1 in let 'Interval l2 u2 := i2 in Interval (add_itv_boundl_subdef l1 l2) (add_itv_boundr_subdef u1 u2).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed