fact: Fixpoint drop A (n:nat) (l:list A) : list A := match n with | 0 => l | S n' => match l with | nil => nil | a::l' => drop n' l' end end.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)