proposition: Lemma fmodV : {morph fmod : x / x^-1%g >-> - x}.
proof: Proof. move=> x; apply: val_inj; rewrite fmvalN !fmodKcond groupV. by case: (x \in A); rewrite ?invg1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)