proposition: Theorem gpow_i: forall n m, 0 <= n -> 0 <= m -> gpow n = gpow (n + m) -> gpow m = G.(e).
proof: Proof. intros n m H1 H2 H3; generalize gpow_in; intro PI. apply g_cancel_l with (g:= G) (a := gpow n); sauto. rewrite <- gpow_add; try rewrite <- H3; sauto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange