proposition: Lemma Zmull_cons: forall a l, Zmull (List.cons a l) = (a * (Zmull l))%positive.
proof: Proof. intros a l. assert (F1:= Pmult_assoc). assert (F2:= Pmult_comm). unfold Zmull. repeat rewrite List.fold_symmetric; simpl; auto; intros; rewrite F2; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod