proposition: Lemma zdrop_product : forall (x : Z) (l : Zlist), inlist Z x l -> (x * zproduct (zdrop x l))%Z = zproduct l.
proof: Proof. simple induction l. simpl in |- *. intro. elim H. intros h t IH. elim (zeqdec x h). intros. rewrite zdrop_head_eq. rewrite H. reflexivity. assumption. intros. rewrite zdrop_head_neq. simpl in |- *. rewrite Zmult_assoc. rewrite Zmult_comm with x h. rewrite Zmult_assoc_reverse. rewrite IH. reflexivity. elim inlist_head_neq with Z x h t. intros. apply H1. assumption. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ