proposition: Lemma odd_perm_prod ts : all dpair ts -> odd_perm (\prod_(t <- ts) tperm t.1 t.2) = odd (size ts).
proof: Proof. elim: ts => [_|t ts IHts] /=; first by rewrite big_nil odd_perm1. by case/andP=> dt12 dts; rewrite big_cons odd_mul_tperm dt12 IHts. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)