proposition: Lemma take_app_l : forall n l l', (n <= length l) -> take n (l ++ l') = take n l.
proof: Proof. Proof using. induction n; destruct l; introv H; rew_list in *; auto. { false. math. } { do 2 rewrite take_cons. fequals. applys IHn. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)