proposition: Lemma add_inum_subproof (xi yi : interval int) (x : {itv R & xi}) (y : {itv R & yi}) (r := add_itv_subdef xi yi) : Itv.spec r (x%:inum + y%:inum).
proof: Proof. rewrite {}/r. move: xi x yi y => [lx ux] [x /= /andP[xl xu]] [ly uy] [y /= /andP[yl yu]]. rewrite /Itv.itv_cond in_itv; apply/andP; split. - move: lx ly xl yl => [xb lx | //] [yb ly | //]. by move: xb yb => [] []; rewrite /Order.le/= rmorphD/=; do ?[exact: lerD|exact: ler_ltD|exact: ltr_leD|exact: ltrD]. - move: ux uy xu yu => [xb ux | //] [yb uy | //]. by move: xb yb => [] []; rewrite /Order.le/= rmorphD/=; do ?[exact: lerD|exact: ler_ltD|exact: ltr_leD|exact: ltrD]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed