proposition: Theorem gpow_add: forall n m, 0 <= n -> 0 <= m -> gpow (n + m) = op (gpow n) (gpow m).
proof: Proof. intros n; case n. intros m _ _; simpl; apply sym_equal; apply e_is_zero_l; apply gpow_in. 2: intros p m H; contradict H; auto with zarith. intros p1 m; case m. intros _ _; simpl; apply sym_equal; apply e_is_zero_r. exact (gpow_in (Zpos p1)). 2: intros p2 _ H; contradict H; auto with zarith. intros p2 _ _; simpl. rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos A x y p2)); auto. exact (gpow_in (Zpos p2)). Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange