proposition: Theorem mkZp_aux_in: forall m p, 0 <= p <= Z_of_nat m -> In p (mkZp_aux m).
proof: Proof. intros m; elim m. simpl; auto with zarith. intros n1 Rec p (H1, H2); case Zle_lt_or_eq with (1 := H2); clear H2; intro H2. rewrite inj_S in H2. simpl; right; apply Rec; split; auto with zarith. rewrite H2; simpl; auto. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression