proposition: Lemma linvseqP s t : reflect (forall i, i < size s -> nth (size s) t (nth (size t) s i) = i) (linvseq s t).
proof: Proof. rewrite /linvseq; apply: (iffP idP) => /=. - move=> /allP H i Hi. by apply/eqP; apply: H; rewrite mem_iota. - move=> H; apply/allP => /= i; rewrite mem_iota /= add0n => Hi. by rewrite (H i Hi). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp