proposition: Theorem zpmult_internal: forall p q, (In (zpmult p q) mL).
proof: Proof. intros p q; unfold zpmult; case (pmult p q); intros z y; apply mL_in; auto with zarith. apply Z_mod_lt; auto with zarith. apply Z_mod_lt; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup