proposition: Lemma compreN T (h : R -> \bar R) (f : T -> R) : {morph h : x / (- x)%R >-> (- x)%E} -> h \o (\- f)%R = \- (h \o f)%E.
proof: Proof. by move=> mh; apply/funext => t /=; rewrite mh. 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