proposition: Lemma zmod_abelian (A : {set U}) : abelian A.
proof: Proof. by apply/centsP=> x _ y _; apply: zmod_mulgC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)