proposition: Lemma list_neq_nil_inv_last : forall l, l <> nil -> exists x q, l = q & x.
proof: Proof. Proof using. introv N. destruct* (@last_case l). Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)