proposition: Lemma itv_continuous_inj_ge f (I : interval R) : (exists x y, [/\ x \in I, y \in I, x < y & f y <= f x]) -> {within [set` I], continuous f} -> {in I &, injective f} -> {in I &, {mono f : x y /~ x <= y}}.
proof: Proof. move=> [a [b [aI bI ab fbfa]]] fC fI x y xI yI. suff : (- f) y <= (- f) x = (y <= x) by rewrite lerNl opprK. apply: itv_continuous_inj_le xI => // [|x1 x1I | x1 x2 x1I x2I]. - by exists a, b; split => //; rewrite lerNl opprK. - by apply/continuousN/fC. by move/oppr_inj; apply/fI. 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)