proposition: Theorem perm_stdE u v : perm_eq u v -> std u = std v -> u = v.
proof: Proof. Proof using. move=> Hperm. move Hn : (size v) => n; elim: n u v Hn Hperm => [| n IHn] u v Hn Hperm /=. move: Hperm => /perm_size; rewrite Hn => /eqP/nilP -> _. by move: Hn => /eqP/nilP ->. move=> Hstd. have:= size_rembig v; rewrite Hn /= => Hszrem. have Hpermrem := perm_rembig Hperm. have:= congr1 rembig Hstd; rewrite -!std_rembig => Hstdrem. move/(_ _ _ Hszrem Hpermrem Hstdrem) : IHn => Hrem {Hszrem Hpermrem Hstdrem}. have:= congr1 posbig Hstd; rewrite !std_posbig => Hstdpos. have:= Hn; case Hv : v => [// | v0 v'] /= _. have:= Hperm => /perm_size; rewrite Hn. case Hu : u => [// | u0 u'] /= _. rewrite -[u0 :: u'](posbig_take_dropE) -[v0 :: v'](posbig_take_dropE). rewrite -Hu -Hv Hrem Hstdpos; congr (_ ++ _ :: _). by apply maxL_perm; rewrite -Hu -Hv. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp