proposition: Lemma prod_correct m n : [prod_num m n] = ([m] * [n])%Z.
proof: Proof. induction n as [ | a n Hrec]; unfold prod_num; fold prod_num. nrom; ring. generalize (scal_correct a m); case scal_num; nrom. rewrite Hrec; intros HH. rewrite Zmult_plus_distr_r, (Zmult_comm [m]), (Zmult_comm [m]), <-HH; ring. intros i l; nrom; intros HH. rewrite add_correct, Hrec, Zmult_plus_distr_r, Zplus_assoc, HH; ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63