proposition: Lemma eq_invP (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. split. - rewrite /eq_inv /versions; move=> [Hsz H] i j /=. apply/idP/idP => /andP[Hij Hnth]. + by rewrite -(H _ _ Hij) -Hsz Hij. + by rewrite H Hsz Hij. - move=> H; have Hsz:= eq_inv_size H; split; first exact Hsz. move=> i j Hij. by move: H; rewrite /eq_inv /versions -Hsz => /(_ i j); rewrite Hij. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp