proposition: Theorem mkZp_aux_length: forall m, length (mkZp_aux m) = (m + 1)%nat.
proof: Proof. intros m; elim m; simpl; auto. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression