proposition: Lemma cymap_comp (U V W: finType) (u : {perm U}) (v : {perm V}) (w : {perm W}) (CMuv : porbits_map u v) (CMvw : porbits_map v w) (CMuw : porbits_map u w) : {in porbits u, CMvw \o CMuv =1 CMuw} -> (cymap CMvw) \o (cymap CMuv) =1 (cymap CMuw).
proof: Proof. Proof using. move=> Hcomp x; rewrite /cymap /=. rewrite /cymapcan /= porbit_perm porbit_cymapcan indporbit_cymap; congr (_ _). have /= -> := (Hcomp (porbit u x)); last exact: imset_f. case: (pickP (mem (CMuw _))) => // Habs; exfalso. have:= fs_porbitP CMuw x => /imsetP[z _ Hz]. by have:= Habs z; rewrite Hz /= porbit_id. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(tuple finfun finset path bigop) mathcomp(fingroup perm action) mathcomp(ssralg matrix mxalgebra algC classfun) partition tools sorted permcomp fibered_set cycles