proposition: Lemma drop_app_length : forall l l', drop (length l) (l ++ l') = l'.
proof: Proof. Proof using. intros. unfold drop, length. rew_to_nat_nonneg~. apply LibList.drop_app_length. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)