proposition: Lemma multdrop_cons_eq : forall (q : nat) (l : natlist), multDrop q (Cons nat q l) = product l.
proof: Proof. unfold multDrop in |- *. simpl in |- *. intros. elim (beq_nat_eq q q). intros. rewrite H. reflexivity. reflexivity. Qed.
imports: Arith ZArith EqNat dec natZ