proposition: Lemma take_drop_last_length : forall l l' x, (l',x) = take_drop_last l -> l <> nil -> length l' = length l - 1.
proof: Proof. Proof using. introv E N. forwards: take_drop_last_spec E N. subst l. rewrite length_last. math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)