proposition: Lemma is_total_action : is_action setT to.
proof: Proof. split=> [a | x a b _ _] /=; last by rewrite toM. by apply: can_inj (to^~ a^-1) _ => x; rewrite -toM ?mulgV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)