proposition: Lemma productzproduct : forall l : natlist, Z_of_nat (product l) = zproduct (map nat Z Z_of_nat l).
proof: Proof. simple induction l. simpl in |- *. reflexivity. intros h t IH. simpl in |- *. rewrite <- IH. rewrite Znat.inj_mult. reflexivity. Qed.
imports: Arith ZArith EqNat dec natZ