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