proposition: Lemma size_leq_invseq s t : linvseq s t -> size s <= size t.
proof: Proof. move=> Hinv; have:= Hinv => /linvseqP H. apply: size_all_leq => i Hi; move/(_ i Hi) : H => <-. by apply: mem_nth; apply: linvseq_ltn_szt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp