proposition: Lemma prod_tpermP s : {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.
proof: Proof. have [n] := ubnP #|[pred x | s x != x]|; elim: n s => // n IHn s /ltnSE-le_s_n. case: (pickP (fun x => s x != x)) => [x s_x | s_id]; last first. exists nil; rewrite // big_nil; apply/permP=> x. by apply/eqP/idPn; rewrite perm1 s_id. have [|ts def_s ne_ts] := IHn (tperm x (s^-1 x) * s); last first. exists ((x, s^-1 x) :: ts); last by rewrite /= -(canF_eq (permK _)) s_x. by rewrite big_cons -def_s mulgA tperm2 mul1g. rewrite (cardD1 x) !inE s_x in le_s_n; apply: leq_ltn_trans le_s_n. apply: subset_leq_card; apply/subsetP=> y. rewrite !inE permM permE /= -(canF_eq (permK _)). have [-> | ne_yx] := eqVneq y x; first by rewrite permKV eqxx. by case: (s y =P x) => // -> _; rewrite eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)