proposition: Theorem mkZp_aux_ulist: forall m, ulist (mkZp_aux m).
proof: Proof. intros m; elim m; simpl; auto. intros m1 H; apply ulist_cons; auto. change (~ In (Z_of_nat (S m1)) (mkZp_aux m1)). rewrite inj_S; intros H1. case in_mkZp_aux with (1 := H1); auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression