proposition: Lemma strict_monotone_fun_revb f r r': strict_monotone_fun f r r' -> strict_monotone_fun f (opp_order r) r'.
proof: Proof. case; first by right; apply: strict_increasing_fun_revb. by left; apply: strict_decreasing_fun_revb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)