proposition: Lemma linvseq_ltn_szt s t : linvseq s t -> forall i, i < size s -> nth (size t) s i < size t.
proof: Proof. move/linvseqP => Hinv i Hi; move/(_ i Hi) : Hinv. case: (ltnP (nth (size t) s i) (size t)) => //= Habs. rewrite (nth_default _ Habs) => H. by move: Hi; rewrite H ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp