proposition: Lemma opp_inum_subproof (i : interval int) (x : {itv R & i}) (r := opp_itv_subdef i) : Itv.spec r (- x%:inum).
proof: Proof. rewrite {}/r; move: i x => [l u] [x /= /andP[xl xu]]; apply/andP; split. - by case: u xu => [[] b i | [] //] /=; rewrite /Order.le/= mulrNz; do ?[by rewrite lerNl opprK|by rewrite ltrNl opprK]. - by case: l xl => [[] b i | [] //] /=; rewrite /Order.le/= mulrNz; do ?[by rewrite ltrNl opprK|by rewrite lerNl opprK]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed