proposition: Lemma take_drop_last_cons : forall (x:A) (l: list A), take_drop_last (x::l) = match l with | nil => (nil, x) | _::_ => let (t, y) := take_drop_last l in (x :: t, y) end.
proof: Proof. Proof using. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)