proposition: Lemma igraph_domain r: sgraph r -> domain (inverse_graph r) = range r.
proof: Proof. move=> gr;rewrite - {2} (igraph_involutive gr) igraph_range //. apply: igraph_graph. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)