proposition: Lemma segment_continuous_le_surjective a b f : a <= b -> f a <= f b -> {within `[a, b], continuous f} -> set_surj `[a, b] `[f a, f b] f.
proof: Proof. move=> le_ab f_ab /(segment_continuous_surjective le_ab). by rewrite (min_idPl _)// (max_idPr _). 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)