proposition: Lemma eq_inv_inversionP (w1 : seq S) (w2 : seq T) : (size w1 = size w2 /\ forall i j, i <= j < size w1 -> (nth inh w1 i > nth inh w1 j) = (nth inh w2 i > nth inh w2 j))%O <-> (eq_inv w1 w2).
proof: Proof. rewrite -eq_invP; split => [][Hsz H]; split; try exact Hsz. - by move=> i j Hij; rewrite !leNgt; rewrite H. - by move=> i j Hij; rewrite !ltNge; rewrite H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp