proposition: Lemma at_rightN a : (- a)^'+ = -%R @ a^'-.
proof: Proof. rewrite /at_right withinN [X in within X _](_ : _ = [set u | u < a])//. rewrite (@fun_predC _ -%R)/=; last exact: opprK. by rewrite image_id; under eq_fun do rewrite ltrNl opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule