proposition: Lemma compf_inverse: {morph inverse_fun : a b / a \co b >-> b \co a}.
proof: Proof. by move=> a b; rewrite /inverse_fun /compose; aw; rewrite compg_inverse. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)