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. unfold take, length in *. rew_to_nat_nonneg~. applys~ LibList.take_app_r. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)