proposition: Theorem gpow_e: forall (A : Set) (op : A -> A -> A) (G : FGroup op) n, 0 <= n -> gpow G.(e) G n = G.(e).
proof: Proof. intros A op G n; case n; simpl; auto with zarith. intros p _; elim p; simpl; auto; intros p1 Rec; repeat rewrite Rec; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange