proposition: Lemma length_eltr (i : 'I_n0) : length 's_i = 1%N.
proof: Proof. Proof using. pose il := lift ord_max i. have Hi : il < n0 by rewrite /il lift_max ltn_ord. have:= length_add1L (s := 1) Hi; rewrite mulg1 length1 lift_max; apply. by rewrite !perm1 /= /bump (leqNgt n0 i) ltn_ord /= add0n inordK // ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr