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