proposition: Theorem Zorder_pos: forall p n, 0 <= Zorder p n.
proof: Proof. intros p n; unfold Zorder. case (Z_le_dec n 1); auto with zarith. intros n1. apply Zlt_le_weak; apply e_order_pos. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression