fact: Definition olast a (l : list a) : Maybe a := let fix go res xs := match xs with | nil => res | cons x xs => go (Just x) xs end in go Nothing l.
imports: Hask.Ltac Hask.Control.Monad Hask.Data.Eq Hask.Data.Maybe Coq.Program.Wf Coq.Sorting.Sorted Coq.Classes.RelationClasses Coq.Lists.List