proposition: Lemma one_step (g : {ffun 'I_k -> 'I_l}) : injective g -> minor id g A * minor g id B = \sum_(fz : Z | good g fz.1) weight fz.1 fz.2.
proof: Proof. move => hg. rewrite split_sumZ_fs from_good_to_perm //=. pose sigma (phi pi: 'S_k) : 'S_k := (phi^-1 * pi)%g. transitivity (\sum_(phi: 'S_k) \sum_(pi : 'S_k) ( ((-1)^+ phi * \prod_i (A i (g (phi i)))) * ((-1)^+ (sigma phi pi) * \prod_i (B (g i) (sigma phi pi i))) ) ); last first. - apply/eq_big => // phi _. apply/eq_big => // pi _. have hinj : injective (finfun (g \o phi)). + have htemp : injective (g \o phi) by apply: inj_comp => //; apply: perm_inj. move => x y; rewrite !ffunE => heq. by apply: htemp. rewrite (@step_weight g (finfun (g \o phi)) pi hinj phi) //. by move => x; rewrite ffunE. transitivity( \sum_(phi: 'S_k) ((-1) ^+ phi * \big[*%R/1]_i A i (g (phi i)) * ( \big[+%R/0]_pi ((-1) ^+ sigma phi pi * \big[*%R/1]_i B (g i) ((sigma phi pi) i))))); last first. - apply/eq_big => // phi _. by rewrite -big_distrr /=. rewrite big_distrl /=. apply/eq_big => // phi _. congr ( _ * _). - by congr (_ * _); apply/eq_big => // i _; rewrite mxE. have inj_s : injective (sigma phi). - rewrite /sigma => p1 p2 /permP heq. apply/permP => x. move: (heq (phi x)). by rewrite !permE /= /invg /= permK. rewrite /minor /determinant. rewrite (reindex_inj inj_s) /=. apply/eq_big => // pi _. congr (_ * _). apply/eq_big => // i _. by rewrite !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor