proposition: Lemma last_case : forall l, l = nil \/ exists x l', l = l' & x.
proof: Proof. Proof using. intros. destruct l. { left*. } { right. forwards* (x&l'&H): (length_pos_inv_last (a::l)). rew_list. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)