proposition: Lemma drop_at_length : forall l, drop (length l) l = nil.
proof: Proof. Proof using. intros. lets H: (@drop_app_length l nil). rew_list~ in H. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)