proposition: Lemma strict_increasing_w f r r': strict_increasing_fun f r r' -> increasing_fun f r r'.
proof: Proof. move=> [or or' [ ff sr sr'] rel]; split => // x y h. case: (equal_or_not x y) => xy. rewrite - xy; order_tac; rewrite - sr'; Wtac; rewrite sr; order_tac. exact: (proj1 (rel _ _ (conj h xy))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)