proposition: Lemma actK : right_loop invg to.
proof: Proof. by move=> a; apply: actKin; rewrite inE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)