proposition: Lemma linvseq_subset_iota s t : linvseq s t -> {subset iota 0 (size s) <= t}.
proof: Proof. move/linvseqP => Hinv i. rewrite mem_iota /= add0n => Hi. move/(_ i Hi) : Hinv => Heq; rewrite -Heq. apply: mem_nth; move: Hi; apply: contraLR; rewrite -!ltnNge !ltnS => H. have := nth_default (size s) H. by rewrite Heq => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp