proposition: Lemma drop_drop : forall l n m, n >= 0 -> m >= 0 -> drop n (drop m l) = drop (n+m) l.
proof: Proof. Proof using. introv Hn Hm. rewrite* <- (to_nat_nonneg Hn). rewrite* <- (to_nat_nonneg Hm). unfold drop. applys_eq LibList.drop_drop. fequals. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)