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: Coq.Sorting.Sorted Coq.Sorting.Permutation Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.List Category.Theory.Coq.Maybe