proposition: Lemma fmodM : {in A &, {morph fmod : x y / (x * y)%g >-> x + y}}.
proof: Proof. by move=> x y Ax Ay /=; apply: val_inj; rewrite /fmod morphM. 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)