proposition: Lemma chain_list_app_inv l m x z : chain_list (l++m) x z -> exists y, chain_list l x y /\ chain_list m y z.
proof: Proof. revert x; induction l as [ | a l IHl ]; intros x. + exists x; simpl; split; auto; constructor. + simpl; intros H; apply chain_list_cons_inv in H. destruct H as (-> & b & H1 & H2). apply IHl in H2; destruct H2 as (y & H2 & H3). exists y; split; auto; constructor 2 with b; auto. Qed.
imports: Arith List Lia