proposition: Lemma take_is_prefix : forall n l, exists q, l = take n l ++ q.
proof: Proof. Proof using. intros n l. gen n. induction l; intros. { exists (@nil A). rewrite~ take_nil. } { destruct n as [|n']. { rewrite take_zero. exists~ (a::l). } { rewrite take_succ. forwards (q'&E): IHl n'. exists q'. rew_list. congruence. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)