proposition: Lemma take_app_r : forall n l l', (n >= length l) -> take n (l ++ l') = l ++ take (n - length l) l'.
proof: Proof. Proof using. intros. gen n. induction l; introv H. { rewrite length_nil in *. do 2 rewrite app_nil_l. fequals. math. } { rewrite length_cons in *. destruct n as [|n']. { false. math. } { rew_list. rewrite take_cons. fequals. applys IHl. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)