[STATEMENT]
lemma fpxs_X_power_mult: "fpxs_X_power (rat_of_nat n * m) = fpxs_X_power m ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fpxs_X_power (rat_of_nat n * m) = fpxs_X_power m ^ n
[PROOF STEP]
by (induction n) (auto simp: ring_distribs fpxs_X_power_add)