[STATEMENT]
lemma of_comp_add:
  fixes a b :: "'a :: monoid_add"
  shows "of_comp (a + b) = of_comp a + of_comp b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_comp (a + b) = of_comp a + of_comp b
[PROOF STEP]
by simp