proposition: Lemma inc_surj_image_segmentP a b f : a <= b -> {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f -> forall y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in `[f a, f b]).
proof: Proof. move=> /inc_surj_image_segment/[apply]/[apply]/predeqP + y => /(_ y) fab. by apply/(equivP idP); symmetry. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule