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: 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