apply add_assoc
case right
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ q + q' + q'' = q + (q' + q'')
no goals