proposition: Lemma order_isomorphism_opposite g r r': order_isomorphism g r r' -> order_isomorphism g (opp_order r) (opp_order r').
proof: Proof. rewrite /order_isomorphism; move=> [pa pb [pc pd pe] pf]. move: (opp_osr pa) (opp_osr pb) => [qa qb] [qc qd]. split => //; first by split => //; ue. move => x y xsg ysg. transitivity (gle r y x) ; first by apply /igraph_pP. transitivity (gle r' (Vf g y) (Vf g x)); first by apply/(pf _ _ ysg xsg). symmetry; apply /igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)