proposition: Lemma length_prods (w : seq 'I_n0) : length 's_[w] <= size w.
proof: Proof. Proof using. elim: w => [/=| w0 w]; first by rewrite big_nil length1. rewrite big_cons /=; move: ('s_[w]) => /= s Hlen. pose w0' := inord (n' := n0) w0. have Hw0' : w0' < n0 by rewrite /= inordK //; apply: ltnW; rewrite ltnS. have -> : w0 = w0' :> nat by rewrite inordK //; apply ltnW; rewrite ltnS. case (ltngtP (s w0') (s (inord w0'.+1))) => H. - by rewrite (length_add1L Hw0' H); rewrite ltnS. - move: Hlen; rewrite (length_sub1L Hw0' H) => /ltnW. by rewrite -ltnS => /ltnW. - exfalso; move/val_inj/perm_inj/(congr1 val)/eqP : H. by rewrite /= inordK // ieqi1F. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr