[STATEMENT]
lemma fpxs_val_power [simp]:
  fixes f :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs"
  assumes "f \<noteq> 0 \<or> n > 0"
  shows "fpxs_val (f ^ n) = of_nat n * fpxs_val f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
proof (cases "f = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
 2. f \<noteq> 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f \<noteq> 0

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
 2. f \<noteq> 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
have [simp]: "f ^ n \<noteq> 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ^ n \<noteq> 0
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

goal (1 subgoal):
 1. f ^ n \<noteq> 0
[PROOF STEP]
by (induction n) auto
[PROOF STATE]
proof (state)
this:
f ^ ?n \<noteq> 0

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
 2. f \<noteq> 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f ^ ?n \<noteq> 0

goal (1 subgoal):
 1. fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
f ^ ?n \<noteq> 0
f \<noteq> 0

goal (1 subgoal):
 1. fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
by (induction n) (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f

goal (1 subgoal):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
qed (use assms in \<open>auto simp: power_0_left\<close>)