proposition: Lemma itv_continuous_inj_mono f (I : interval R) : {within [set` I], continuous f} -> {in I &, injective f} -> monotonous I f.
proof: Proof. move=> fC fI. case: (pselect (exists a b, [/\ a \in I , b \in I & a < b])); last first. move=> N2I; left => x y xI yI; suff -> : x = y by rewrite ?lexx. by apply: contra_notP N2I => /eqP; case: ltgtP; [exists x, y|exists y, x|]. move=> [a [b [aI bI lt_ab]]]. have /orP[faLfb|fbLfa] := le_total (f a) (f b). by left; apply: itv_continuous_inj_le => //; exists a, b; rewrite ?faLfb. by right; apply: itv_continuous_inj_ge => //; exists a, b; rewrite ?fbLfa. 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)