proposition: Theorem pow_S: forall k n, k ^ (S n) = k * k ^ n.
proof: Proof. intros k n; simpl; auto; case n; auto. simpl; rewrite Eth.(Kfth).(F_R).(Rmul_comm). rewrite Eth.(Kfth).(F_R).(Rmul_1_l); auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith