proposition: Lemma zmultdrop_cons_eq : forall (q : Z) (l : Zlist), zmultDrop q (Cons Z q l) = zproduct l.
proof: Proof. unfold zmultDrop in |- *. simpl in |- *. intros. elim (zeq_bool_eq q q). intros. rewrite H. reflexivity. reflexivity. Qed.
imports: Arith ZArith EqNat dec natZ