proposition: Lemma take_is_prefix : forall n l, exists q, l = take n l ++ q.
proof: Proof. Proof using. intros. unfold take. applys~ LibList.take_is_prefix. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)