fact: Definition cycle_dec s : {set {perm T}} := perm_dec (porbit_set s) s.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp