proposition: Lemma rembig_catR a u b v : maxL a u <= maxL b v -> rembig (a :: u ++ b :: v) = a :: u ++ rembig (b :: v).
proof: Proof. Proof using. rewrite /=; elim: u a => [| u0 u IHu] a. by rewrite allLtnConsE /= leNgt /= => /negbTE ->. rewrite allLtnConsE maxL_cat /= -maxXL ge_max => /andP[Ha Hmax]. by rewrite ltNge le_max Ha orbT /= -(IHu _ Hmax). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools