proposition: Lemma perm_rembig u v : perm_eq u v -> perm_eq (rembig u) (rembig v).
proof: Proof. Proof using. case Hu: u => [/= | u0 u']; case Hv: v => [//= | v0 v']. - by move=> /perm_size /=. - by move=> /perm_size /=. move=> Hperm; have Hmax:= maxL_perm Hperm; move: Hmax Hperm. have/(congr1 rembig):= Hu => /eqP/rembigP Htmp. have {}/Htmp : u0 :: u != [::] by []. move=> [u1] [bu] [u2] []; rewrite {1}Hu => -> Hub Hlequ Hltnu. rewrite (maxL_LbR Hub Hlequ (allLtnW Hltnu)) {Hlequ Hltnu}. rewrite Hub {u Hu Hub u0 u'}. have/(congr1 rembig):= Hv => /eqP/rembigP Htmp. have {}/Htmp : v0 :: v != [::] by []. move=> [v1] [bv] [v2] []; rewrite {1}Hv => -> Hvb Hleqv Hltnv. rewrite (maxL_LbR Hvb Hleqv (allLtnW Hltnv)) {Hleqv Hltnv}. rewrite Hvb {v Hv Hvb v0 v'}. rename bv into mx; move ->. rewrite -[mx :: u2]cat1s -[mx :: v2]cat1s. rewrite -[perm_eq (u1 ++ u2) _](perm_cons mx). have Hlemma u v : perm_eq (u ++ [:: mx] ++ v) (mx :: u ++ v). rewrite catA -[mx :: u ++ v]/((mx :: u) ++ v) perm_cat2r -[mx :: u]cat1s. apply: permEl; exact: perm_catC. move=> H; have:= Hlemma u1 u2; rewrite perm_sym. move/perm_trans; apply. by apply: (perm_trans H); apply: Hlemma. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools