proposition: Lemma take_drop_last_spec : forall (x:A) (l l': list A), (l',x) = take_drop_last l -> l <> nil -> l = l' & x.
proof: Proof. Proof using. induction l as [|a t]; introv E N. false. rewrite take_drop_last_cons in E. destruct (take_drop_last t) as [u r]. { destruct t; inverts E. rewrite* app_nil_l. rew_list. fequals. applys IHt; auto_false*. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)