proposition: Lemma rembig_eq_permR u v1 v2 : perm_eq v1 v2 -> (rembig (u ++ v1) = (rembig u) ++ v1 /\ rembig (u ++ v2) = (rembig u) ++ v2) \/ (rembig (u ++ v1) = u ++ (rembig v1) /\ rembig (u ++ v2) = u ++ (rembig v2)).
proof: Proof. Proof using. case: v2 => [| b2 v2]. by move/perm_size => /eqP /= /nilP ->; left; rewrite !cats0. case: v1 => [//= | b1 v1]; first by move/perm_size. case: u => [//= | a u]; first by right. move/maxL_perm => Heq. case (leP (maxL a u) (maxL b1 v1)) => 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