proposition: Lemma oppr_itv ba bb (xa xb x : R) : (- x \in Interval (BSide ba xa) (BSide bb xb)) = (x \in Interval (BSide (~~ bb) (- xb)) (BSide (~~ ba) (- xa))).
proof: Proof. by rewrite !itv_boundlr /<=%O /= !implybF negbK andbC lteifNl lteifNr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)