proposition: Lemma zproductproduct : forall l : Zlist, Z.abs_nat (zproduct l) = product (map Z nat Z.abs_nat l).
proof: Proof. simple induction l. simpl in |- *. reflexivity. intros h t IH. simpl in |- *. rewrite abs_mult. rewrite IH. reflexivity. Qed.
imports: Arith ZArith EqNat dec natZ