proposition: Lemma segment_can_le a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> {in `[f a, f b] &, {mono g : x y / x <= y}}.
proof: Proof. move=> aLb ctf fK; have [fbLfa | faLfb] := ltrP (f b) (f a). by move=> x y; rewrite itv_ge// -ltNge. have [aab bab] : a \in `[a, b] /\ b \in `[a, b] by rewrite !bound_itvE. case: ltgtP faLfb => // [faLfb _|-> _ _ _ /itvxxP-> /itvxxP->]; rewrite ?lexx//. have lt_ab : a < b by case: (ltgtP a b) aLb faLfb => // ->; rewrite ltxx. have w : exists x y, [/\ x \in `[a, b], y \in `[a, b], x < y & f x <= f y]. by exists a, b; rewrite !bound_itvE (ltW faLfb). have fle := itv_continuous_inj_le w ctf (can_in_inj fK). move=> x y xin yin; have := IVT aLb ctf. case: (ltrgtP (f a) (f b)) faLfb => // _ _ ivt. by have [[u uin <-] [v vin <-]] := (ivt _ xin, ivt _ yin); rewrite !fK// !fle. 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)