fact: Fixpoint take_drop_last `{IA:Inhab A} (l:list A) : (list A)*A := match l with | nil => arbitrary | x::l' => match l' with | nil => (nil,x) | _ => let (t,y) := take_drop_last l' in (x::t, y) end end.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)