fact: Fixpoint drop (q : nat) (qlist : natlist) {struct qlist} : natlist := match qlist with | Nil => Nil nat | Cons q' l => if beq_nat q q' then l else Cons nat q' (drop q l) end.
imports: Arith ZArith EqNat dec natZ