proposition: Theorem in_mkZp_aux: forall m p, In p (mkZp_aux m) -> 0 <= p <= Z_of_nat m.
proof: Proof. intros m; elim m; clear m. simpl; intros p H1; case H1; clear H1; intros H1; subst; auto with zarith. intros m1; generalize (inj_S m1); simpl. intros H Rec p [H1 | H1]. rewrite <- H1; rewrite H; auto with zarith. rewrite H; case (Rec p); auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression