proposition: Lemma zmultdrop_cons_neq : forall (p q : Z) (l : Zlist), p <> q -> zmultDrop p (Cons Z q l) = (q * zmultDrop p l)%Z.
proof: Proof. unfold zmultDrop in |- *. simpl in |- *. intros. elim (zeq_bool_neq p q). intros. rewrite H0. simpl in |- *. reflexivity. assumption. Qed.
imports: Arith ZArith EqNat dec natZ