proposition: Lemma segment_can_ge a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> {in `[f b, f a] &, {mono g : x y /~ x <= y}}.
proof: Proof. move=> aLb fC fK x y xfbfa yfbfa; rewrite -lerN2. apply: (@segment_can_le (- b) (- a) (f \o -%R) (- g)); rewrite /= ?lerN2 ?opprK //. pose fun_neg : subspace `[-b,-a] -> subspace `[a,b] := itvN_oppr a b. move=> z; apply: (@continuous_comp _ _ _ [fun of fun_neg]); last exact: fC. exact/subspaceT_continuous/continuous_subspaceT/opp_continuous. by move=> z zab; rewrite -[- g]/(@GRing.opp _ \o g)/= fK ?opprK// oppr_itvcc. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)