proposition: Lemma eq_inv_posbig (u : seq S) (v : seq T) : eq_inv u v -> posbig u = posbig v.
proof: Proof. move=> H; have /eqP := eq_inv_size H. elim: u v H => [| a u IHu] /= v. by move=> _; rewrite eq_sym => /nilP ->. case: v => [// |b v] /= Heq. rewrite eqSS => Hsize; move/(_ v (eq_inv_consK Heq) Hsize) : IHu => Hpos. have:= Heq; rewrite /eq_inv /versions => Hinv. rewrite -(eq_inv_allgtnX Heq). by case: (allLtn u a); last by rewrite Hpos. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp