proposition: Lemma segment_continuous_inj_ge f a b : f a >= f b -> {within `[a, b], continuous f} -> {in `[a, b] &, injective f} -> {in `[a, b] &, {mono f : x y /~ x <= y}}.
proof: Proof. move=> fafb fct finj; have [|//] := itv_continuous_inj_mono fct finj. have [aLb|bLa|<-] := ltrgtP a b; first 1 last. - by move=> _ x ?; rewrite itv_ge// -ltNge. - by move=> _ x y /itvxxP-> /itvxxP->; rewrite !lexx. move=> /(_ b a); rewrite !bound_itvE fafb. by move=> /(_ (ltW aLb) (ltW aLb)); rewrite lt_geF. 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)