proposition: Lemma std_eq_inv (u : seq S) (v : seq T) : eq_inv u v -> std u = std v.
proof: Proof. move => Hinv; move Hn : (size u) => n. elim: n u v Hn Hinv => [// | n IHn] u v Hn Hinv. have:= eq_inv_size Hinv. rewrite Hn => /esym/eqP/nilP ->. by move: Hn => /eqP/nilP ->. have Hsz := eq_inv_size Hinv. have Hszremu : size (rembig u) = n by rewrite size_rembig Hn. have Hszremv : size (rembig v) = n by rewrite size_rembig -Hsz Hn. move/(_ (rembig u) (rembig v) Hszremu (eq_inv_rembig Hinv)) : IHn. rewrite /std -Hsz Hn Hszremu Hszremv /= => <-. by rewrite -(eq_inv_posbig Hinv). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp