proposition: Lemma continuous_inj_image_segment a b f : a <= b -> {within `[a, b], continuous f} -> {in `[a, b] &, injective f} -> f @` `[a, b] = f @`[a, b]%classic.
proof: Proof. move=> leab fct finj; apply: mono_surj_image_segment => //. exact: itv_continuous_inj_mono. exact: segment_continuous_surjective. 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)