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