proposition: Lemma opposite_right_directedP r: sgraph r -> (right_directed r <-> left_directed (opp_order r)).
proof: Proof. move=> gr. apply: (iff_trans (right_directedP r)); symmetry. apply: (iff_trans (left_directedP (opp_order r))). split; move=> [or hyp]. move: (opp_osr or) => []. rewrite /opp_order igraph_involutive// => odr sa. split=> // x y xs ys. move: hyp; rewrite - sa => hyp. move: (hyp _ _ xs ys) => [z [xz yz]]. by exists z; split => //;apply/igraph_pP. have [ooi oisr]:= (opp_osr or). split=>//; rewrite oisr; move => x y xs ys. move: (hyp _ _ xs ys)=> [z [ xz yz]]. by exists z;split => //; apply/igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)