proposition: Theorem compgA : associative composeg.
proof: Proof. move => r r' r'';set_extens x. move /compg_P=> [px [y /compg_pP [z pa pb] pc]]. rewrite -px; apply/compg_pP; ex_tac; apply/compg_pP; ex_tac. move /compg_P=> [px [y pa /compg_pP [z pb pc]]]. rewrite -px; apply/compg_pP; ex_tac; apply/compg_pP; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)