proposition: Lemma length1 : length 1 = 0.
proof: Proof. Proof using. rewrite /length /invset. apply/eqP; rewrite cards_eq0; apply/eqP/setP => [[i j]]; rewrite !inE !perm1. apply/negP=> /andP[/ltn_trans /[apply]]. by rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr