proposition: Lemma expg_prod_of_disjoint A C x i: disjoint_psupports A -> C \in A -> x \in psupport C -> ((\prod_(C0 in A) C0) ^+ i) x = (C ^+ i) x.
proof: Proof. Proof using. move => Hdisj HC Hx. have Hin j : (C ^+ j) x \in psupport C. elim j => [|k Hk]; first by rewrite expg0 perm1. by rewrite expgSr permM -psupport_stable. elim: i => [|j Hj]. - by rewrite !expg0 perm1. - by rewrite !expgSr !permM Hj (prod_of_disjoint Hdisj HC (Hin j)). 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