proposition: Lemma olast_spec : forall a (u : a) us, olast (u :: us) = Nothing -> False.
proof: Proof. intros a u. induction us as [|x xs IHxs]; simpl; intros. discriminate. rewrite olast_last in H. rewrite olast_last in IHxs. destruct xs as [|y ys]; discriminate. 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