proposition: Lemma gather_by_strictness : \sum_(g : {ffun 'I_k -> 'I_l} | strictf g) \sum_(fz : Z | good g fz.1) weight fz.1 fz.2 = \sum_(g : {ffun 'I_k -> 'I_l} | strictf g) (minor id g A) * (minor g id B).
proof: Proof. apply/eq_big => // g hg. rewrite one_step //. by apply/inj_strictf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor