proposition: Lemma list_eq_take_app_drop : forall n l, n <= length l -> take n l ++ drop n l = l.
proof: Proof. Proof using. introv H. forwards*: take_app_drop_spec n l. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)