proposition: Theorem gpow_1_more: forall n, 0 < n -> gpow n = G.(e) -> forall m, 0 <= m -> exists p, 0 <= p < n /\ gpow m = gpow p.
proof: Proof. intros n H1 H2 m Hm; generalize Hm; pattern m; apply Z_lt_induction; auto with zarith; clear m Hm. intros m Rec Hm. case (Zle_or_lt n m); intros H3. case (Rec (m - n)); auto with zarith. intros p (H4,H5); exists p; split; auto. replace m with (n + (m - n)); auto with zarith. rewrite gpow_add; try rewrite H2; try rewrite H5; sauto; auto with zarith. generalize gpow_in; sauto. exists m; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange