proposition: Lemma zmultdrop_mult : forall (qlist : Zlist) (q : Z), inlist Z q qlist -> (q * zmultDrop q qlist)%Z = zproduct qlist.
proof: Proof. simple induction qlist. simpl in |- *. intros. elim H. simpl in |- *. intros q1 l IH. intros. elim (zeqdec q q1). intro. rewrite H0. rewrite zmultdrop_cons_eq. reflexivity. intro. rewrite zmultdrop_cons_neq. rewrite <- (IH q). rewrite Zmult_assoc. rewrite (Zmult_comm q q1). rewrite Zmult_assoc. reflexivity. unfold inlist in H. simpl in H. elim H. intro. elim H0. assumption. intro. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ