proposition: Lemma olast_last : forall a (u : a) us, olast (u :: us) = Just (last us u).
proof: Proof. intros a u. induction us as [|x xs IHxs]; simpl; trivial. generalize dependent u. destruct xs as [|y ys]; intros. reflexivity. exact IHxs. Qed.
imports: Hask.Ltac Hask.Control.Monad Hask.Data.Eq Hask.Data.Maybe Coq.Program.Wf Coq.Sorting.Sorted Coq.Classes.RelationClasses Coq.Lists.List