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