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