proposition: Lemma odd_permM : {morph odd_perm : s1 s2 / s1 * s2 >-> s1 (+) s2}.
proof: Proof. move=> s1 s2; case: (prod_tpermP s1) => ts1 ->{s1} dts1. case: (prod_tpermP s2) => ts2 ->{s2} dts2. by rewrite -big_cat !odd_perm_prod ?all_cat ?dts1 // size_cat oddD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)