proposition: Lemma odd_eltr i : (i < n0)%N -> odd_perm 's_i.
proof: Proof. rewrite odd_tperm => Hi. apply/negP=> /eqP/(congr1 val)/eqP/=. rewrite !inordK // ?ltnS ?ieqi1F //. exact: ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr