proposition: Lemma det_perm n (s : 'S_n) : \det (perm_mx s) = (-1) ^+ s :> R.
proof: Proof. rewrite [\det _](bigD1 s) //= big1 => [|i _]; last by rewrite /= !mxE eqxx. rewrite mulr1 big1 ?addr0 => //= t Dst. case: (pickP (fun i => s i != t i)) => [i ist | Est]. by rewrite (bigD1 i) // mulrCA /= !mxE (negPf ist) mul0r. by case/eqP: Dst; apply/permP => i; move/eqP: (Est i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)