proposition: Lemma abelian_cycle_dec s : abelian <<cycle_dec s>>.
proof: Proof. Proof using. by apply abelian_disjoint_psupports; apply disjoint_cycle_dec. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp