proposition: Theorem zpmult_1_l: forall p, In p mL -> zpmult (1, 0) p = p.
proof: Proof. intros p H; case in_mL with (1 := H); clear H; intros p1 (p2, ((H1, H2), (H3, H4))); subst. unfold zpmult; rewrite pmult_1_l. repeat rewrite Zmod_small; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup