proposition: Lemma multdropzmultdrop : forall (q : nat) (qlist : natlist), Z_of_nat (multDrop q qlist) = zmultDrop (Z_of_nat q) (map nat Z Z_of_nat qlist).
proof: Proof. simple induction qlist. simpl in |- *. reflexivity. intros h t. elim (eqdec q h). intro H. rewrite H. simpl in |- *. rewrite multdrop_cons_eq. rewrite zmultdrop_cons_eq. rewrite productzproduct. intro IH. reflexivity. intro H. simpl in |- *. rewrite multdrop_cons_neq. rewrite zmultdrop_cons_neq. intro IH. rewrite <- IH. rewrite Znat.inj_mult. reflexivity. intro. apply H. rewrite <- (abs_inj q). rewrite <- (abs_inj h). rewrite H0. reflexivity. assumption. Qed.
imports: Arith ZArith EqNat dec natZ