[STATEMENT]
lemma lemAddOverScale: 
  shows "a**u \<oplus> b**u = (a+b)**u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ** u \<oplus> b ** u = (a + b) ** u
[PROOF STEP]
by (simp add: semiring_normalization_rules(1))