proposition: Lemma rembig_eq_permL u1 u2 v : perm_eq u1 u2 -> (rembig (u1 ++ v) = (rembig u1) ++ v /\ rembig (u2 ++ v) = (rembig u2) ++ v) \/ (rembig (u1 ++ v) = u1 ++ (rembig v) /\ rembig (u2 ++ v) = u2 ++ (rembig v)).
proof: Proof. Proof using. case: u2 => [| a2 u2]; first by move/perm_size => /eqP /= /nilP ->; right. case: u1 => [| a1 u1]; first by move/perm_size. case: v => [/= | b v]; first by rewrite /= !cats0; left. move/maxL_perm => Heq. case (leP (maxL a1 u1) (maxL b v)) => H1; have := H1; rewrite Heq => H2. - by right; rewrite (rembig_catR H1) (rembig_catR H2). - by left; rewrite (rembig_catL H1) (rembig_catL H2). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools