proposition: Lemma rembig_cat u v : rembig (u ++ v) = (rembig u) ++ v \/ rembig (u ++ v) = u ++ (rembig v).
proof: Proof. Proof using. case: u => [/= | a u]; first by right. case: v => [/= | b v]; first by rewrite !cats0; left. case (leP (maxL a u) (maxL b v)) => Hcase. - by rewrite (rembig_catR Hcase); right. - by rewrite (rembig_catL Hcase); left. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools