[STATEMENT]
lemma fpxs_val_minus_commute: "fpxs_val (f - g) = fpxs_val (g - f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fpxs_val (f - g) = fpxs_val (g - f)
[PROOF STEP]
by (subst fpxs_val_uminus [symmetric]) (simp del: fpxs_val_uminus)