proposition: Lemma compg_domain r r': sgraph r' -> domain (r' \cg r) = inverse_image r (domain r').
proof: Proof. move=>gr; have cg:= (@compg_graph r' r); set_extens t. move/(domainP cg) => [y /compg_pP [z pa pb]]. apply/iim_graph_P; ex_tac; ex_tac. move/iim_graph_P => [x /(domainP gr) [y pa] pb]. apply/(domainP cg); exists y; apply /compg_pP; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)