proposition: Lemma opposite_left_directedP r: sgraph r -> (left_directed r <-> right_directed (opp_order r)).
proof: Proof. move=>g; symmetry. have go: sgraph (opp_order r) by fprops. move:(opposite_right_directedP go). by rewrite /opp_order (igraph_involutive g). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)