proposition: Lemma Last_app : forall (x:A) (l1 l2:list A), Last x l2 -> Last x (l1 ++ l2).
proof: Proof. intros. induction l1. simpl; assumption. change ((a :: l1) ++ l2) with (a :: (l1 ++ l2)). apply Last_step; assumption. Qed.
imports: Coq(List) Coq(Arith)