proposition: Lemma odd_size_permE ts : all (gtn n0) ts -> odd (size ts) = odd_perm 's_[ts].
proof: Proof. Proof using. elim: ts => [_ | t0 t IHt] /=; first by rewrite big_nil odd_perm1. move=> /andP[Ht0 {}/IHt ->]. by rewrite big_cons odd_mul_tperm (inordi_neq_i1 Ht0) addTb. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr