proposition: Lemma contract_imageN (S : set (\bar R)) : (@contract R) @` (-%E @` S) = -%R @` ((@contract R) @` S).
proof: Proof. rewrite predeqE => r; split => [[y [z Sz <-{y} <-{r}]]|[s [y Sy <-{s} <-{r}]]]. by exists (contract z); [exists z | rewrite contractN]. by exists (- y); [exists y | rewrite contractN]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal