proposition: Lemma Last_app_inv : forall (x:A) (l1 l2:list A), l2 <> nil -> Last x (l1 ++ l2) -> Last x l2.
proof: Proof. intros. induction l1. simpl; assumption. apply IHl1. apply Last_step_inv with (y := a). destruct l1; [assumption | intuition; discriminate H1]. assumption. Qed.
imports: Coq(List) Coq(Arith)