proposition: Lemma length_add1L s (i : 'I_n) : i < n0 -> s i < s (inord i.+1) -> length ('s_i * s) = (length s).+1.
proof: Proof. Proof using. rewrite /length => Hi Hfwd. rewrite (invset_eltrL Hi Hfwd). rewrite cardsU1 (card_imset _ (@inv_inj _ _ _)); first last. by move=> [u v] /=; rewrite !eltrK. rewrite (_ : (_, _) \in _ = false) //. apply/negP => /imsetP[[u v]]. rewrite inE /= => /andP[Huv Hsvu] []. move/(congr1 's_i); rewrite eltrK eltrL => Hu; subst u. move/(congr1 's_i); rewrite eltrK eltrR => Hv; subst v. by move: Huv => /ltnW; rewrite inordi1 // ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr