proposition: Lemma rembig_catL a u b v : maxL a u > maxL b v -> rembig (a :: u ++ b :: v) = rembig (a :: u) ++ b :: v.
proof: Proof. Proof using. rewrite /=; elim: u a => [| u0 u IHu] a. by rewrite allLtnConsE /= ltNge /= => /negbTE ->. rewrite allLtn_catE !allLtnConsE /= -maxXL maxC /Order.max. case: (ltP (maxL u0 u) a) => [H -> //= | H Hmax /=]. by rewrite IHu. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools