proposition: Lemma igraph_range r: sgraph r -> range (inverse_graph r) = domain r.
proof: Proof. move=> gr; set_extens x; first by move/funI_P => [y /igraphP [_ h] ->]; ex_tac. move/funI_P => [y yi ->]; apply: (range_i (x:=(Q y))); apply/igraph_pP. by rewrite (gr _ yi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)