proposition: Theorem compg_image: action_prop direct_image composeg.
proof: Proof. move => gr_imegr' r x;set_extens t. move /dirim_P => [z zx /compg_pP [u pa pb]]. apply/dirim_P; ex_tac; apply/dirim_P; ex_tac. move /dirim_P => [z /dirim_P [u pa pb] pc]. apply/dirim_P; ex_tac; apply/compg_pP; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)