proposition: Lemma length_drop_nonneg : forall n l, 0 <= n <= length l -> length (drop n l) = length l - n.
proof: Proof. Proof using. introv E. forwards~ (l'&N&M): drop_spec n l. pattern l at 2. rewrite M. rew_list. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)