proposition: Theorem zpmult_0_l: forall p, (zpmult (0, 0) p) = (0, 0).
proof: Proof. intros p; case p; intros x y; unfold zpmult, pmult; simpl. rewrite Zmod_small; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup