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