proposition: Lemma strict_monotone_from_injective f r r': injection f -> monotone_fun f r r' -> strict_monotone_fun f r r'.
proof: Proof. move=> inf; case. by left; apply: strict_increasing_from_injective. by right; apply: strict_decreasing_from_injective. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)