proposition: Theorem gpow_pow: forall (A : Set) (op : A -> A -> A) (a : A) (G : FGroup op), In a (s G) -> forall n, 0 <= n -> gpow a G (2 ^ n) = G.(e) -> forall m, n <= m -> gpow a G (2 ^ m) = G.(e).
proof: Proof. intros A op a G H n H1 H2 m Hm. replace m with (n + (m - n)); auto with zarith. rewrite Zpower_exp; auto with zarith. rewrite gpow_gpow; auto with zarith. rewrite H2; apply gpow_e. apply Zpower_ge_0; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange