proposition: Lemma strict_increasing_fun_revb f r r': strict_increasing_fun f r r' -> strict_decreasing_fun f (opp_order r) r'.
proof: Proof. rewrite /strict_decreasing_fun; move=> [or or' [ ff sr sr'] rel]. move: (opp_osr or) => [pa pb]; split => //; first by saw; ue. by move=> x y /opp_gltP;apply: rel. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)