proposition: Lemma out_perm_prod A x : {in A, forall C, x \notin psupport C} -> (\prod_(C in A) C) x = x.
proof: Proof. Proof using. move=> H. rewrite -big_filter; have [/= S _ [_ mem_S] _] := big_enumP (mem A). have {mem_S}H : {in S, forall C, x \notin psupport C}. by move=> C; rewrite mem_S; apply: H. elim: S H => [| a S IHS HaS]; first by rewrite big_nil perm1. rewrite big_cons permM. have:= HaS _ (mem_head a S); rewrite in_psupport negbK => /eqP ->. rewrite {}IHS // => C HC. by apply: HaS; rewrite in_cons HC orbT. 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