proposition: Lemma cymapK (U V : finType) (u : {perm U}) (v : {perm V}) (CM : porbits_map u v) (CMi : porbits_map v u) : {in porbits u, cancel CM CMi} -> cancel (cymap CM) (cymap CMi).
proof: Proof. Proof using. move=> H x /=. have porbits_stab_id (s : {perm U}) : id @: porbits s \subset porbits s. by rewrite imset_id. pose CMid s := PorbitMap (porbits_stab_id s) (fun x _ => erefl #|x|). rewrite [LHS](cymap_comp (CMuw := (CMid u))); first exact: cymap_id. by move=> y Hy /=; exact: H. 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