proposition: Lemma monotone_fun_revb f r r': monotone_fun f r r' -> monotone_fun f (opp_order r) r'.
proof: Proof. case; first by right; apply: increasing_fun_revb. by left; apply: decreasing_fun_revb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)