proposition: Lemma last_app l1 l2 : last (l1 ++ l2) = match last l2 with Some y => Some y | None => last l1 end.
proof: Proof. destruct l2 as [|x l2 _] using rev_ind. - by rewrite (right_id_L _ (++)). - by rewrite (assoc_L (++)), !last_snoc. Qed.
imports: stdpp(options)