proposition: Lemma segment_dec_surj_continuous a b f : {in `[a, b] &, {mono f : x y /~ x <= y}} -> set_surj `[a, b] `[f b, f a] f -> {within `[a, b], continuous f}.
proof: Proof. move=> fge f_surj; suff: {within `[a, b], continuous (- f)}. move=> contNf x xab; rewrite -[f]opprK. exact/continuous_comp/opp_continuous/contNf. apply: segment_inc_surj_continuous. by move=> x y xab yab; rewrite lerN2 fge. by move=> y /=; rewrite -oppr_itvcc => /f_surj[x ? /(canLR opprK)<-]; exists x. 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)