proposition: Lemma card_perm A : #|perm_on A| = (#|A|)`!.
proof: Proof. pose ffA := {ffun {x | x \in A} -> T}. rewrite -ffactnn -{2}(card_sig [in A]) /= -card_inj_ffuns_on. pose fT (f : ffA) := [ffun x => oapp f x (insub x)]. pose pfT f := insubd (1 : {perm T}) (fT f). pose fA s : ffA := [ffun u => s (val u)]. rewrite -!sum1dep_card -sum1_card (reindex_onto fA pfT) => [|f]. apply: eq_bigl => p; rewrite andbC; apply/idP/and3P=> [onA | []]; first split. - apply/eqP; suffices fTAp: fT (fA p) = pval p. by apply/permP=> x; rewrite -!pvalE insubdK fTAp //; apply: (valP p). apply/ffunP=> x; rewrite ffunE pvalE. by case: insubP => [u _ <- | /out_perm->] //=; rewrite ffunE. - by apply/forallP=> [[x Ax]]; rewrite ffunE /= perm_closed. - by apply/injectiveP=> u v; rewrite !ffunE => /perm_inj; apply: val_inj. move/eqP=> <- _ _; apply/subsetP=> x; rewrite !inE -pvalE val_insubd fun_if. by rewrite if_arg ffunE; case: insubP; rewrite // pvalE perm1 if_same eqxx. case/andP=> /forallP-onA /injectiveP-f_inj. apply/ffunP=> u; rewrite ffunE -pvalE insubdK; first by rewrite ffunE valK. apply/injectiveP=> {u} x y; rewrite !ffunE. case: insubP => [u _ <-|]; case: insubP => [v _ <-|] //=; first by move/f_inj->. by move=> Ay' def_y; rewrite -def_y [_ \in A]onA in Ay'. by move=> Ax' def_x; rewrite def_x [_ \in A]onA in Ax'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)