proposition: Lemma length_sub1L s (i : 'I_n) : i < n0 -> s i > s (inord i.+1) -> length s = (length ('s_i * s)).+1.
proof: Proof. Proof using. move=> Hi Hs. rewrite -{1}[s](mulKg 's_i) eltrV. by apply (length_add1L Hi); rewrite !permM eltrL eltrR. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr