proposition: Theorem pmult_1_l: forall p, In p mkZp -> pmult 1 p = p.
proof: Proof. intros p H; unfold pmult; rewrite Zmult_1_l. apply Zmod_small. case (in_mkZp p); auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression