proposition: Lemma list_cut : forall (l:list A) (x:A), exists b : A, exists l' : list A, x :: l = l' ++ b :: nil.
proof: Proof. intro l; elim l; simpl. intro x; exists x; exists (nil (A:=A)); auto. intros a1 l3 H x. case (H a1). intros x0 H7. case H7; intros b Hb. rewrite Hb. exists x0. exists (x :: b); auto. Qed.
imports: List Arith Lia