proposition: Lemma linvseq_sizeP s t : linvseq s t -> size s = size t -> invseq s t.
proof: Proof. move=> Hinv Hsize; rewrite /invseq; apply/andP; split; first exact Hinv. have Hiota := linvseq_subset_iota Hinv. have Htmp : size t <= size (iota 0 (size s)) by rewrite size_iota Hsize. have Huniq := leq_size_uniq (iota_uniq 0 (size s)) Hiota Htmp. move/(perm_size_uniq (iota_uniq 0 (size s)) Hiota) : Htmp => Hperm {Hiota}. apply/linvseqP => i Hi; move: Hinv => /linvseqP Hinv. have:= mem_nth (size s) Hi; rewrite -(perm_mem Hperm) mem_iota /= add0n => Hnth. move/(_ _ Hnth) : Hinv => Heq. have/eqP := Heq; rewrite nth_uniq //=; first by move/eqP. case: (ltnP (nth (size t) s (nth (size s) t i)) (size t)) => //= H. move: Heq; rewrite (nth_default _ H) => /eqP. by rewrite (gtn_eqF Hnth). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp