proposition: Lemma compreBr T (h : R -> \bar R) (f g : T -> R) : {morph h : x y / (x - y)%R >-> (x - y)%E} -> h \o (f \- g)%R = ((h \o f) \- (h \o g))%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