proposition: Lemma strict_decreasing_from_injective f r r': injection f -> decreasing_fun f r r' -> strict_decreasing_fun f r r'.
proof: Proof. move=> [_ inf] [or or' [ ff sr sr'] rel]; split => //. move=> x y [lexy neq]; split; first by apply: rel. dneg Wxy; apply: inf=>//; rewrite sr; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)