proposition: Lemma app_eq_inv l1 l2 k1 k2 : l1 ++ l2 = k1 ++ k2 → (∃ k, l1 = k1 ++ k ∧ k2 = k ++ l2) ∨ (∃ k, k1 = l1 ++ k ∧ l2 = k ++ k2).
proof: Proof. intros Hlk. destruct (decide (length l1 < length k1)). - right. rewrite <-(take_drop (length l1) k1), <-(assoc_L _) in Hlk. apply app_inj_1 in Hlk as [Hl1 Hl2]; [|rewrite take_length; lia]. exists (drop (length l1) k1). by rewrite Hl1 at 1; rewrite take_drop. - left. rewrite <-(take_drop (length k1) l1), <-(assoc_L _) in Hlk. apply app_inj_1 in Hlk as [Hk1 Hk2]; [|rewrite take_length; lia]. exists (drop (length k1) l1). by rewrite <-Hk1 at 1; rewrite take_drop. Qed.
imports: stdpp(options)