proposition: Lemma odd_perm1 : odd_perm 1 = false.
proof: Proof. rewrite /odd_perm card_imset ?addbb // => x y; move/eqP; rewrite eq_porbit_mem. by rewrite porbit.unlock cycle1 imset_set1 /aperm perm1 inE=> /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)