have := ccl.cocycle_condition q (-q) q
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c q (-q) = q +ᵥ c (-q) q
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q (-q) + c (q + -q) q = q +ᵥ c (-q) q + c q (-q + q)
⊢ c q (-q) = q +ᵥ c (-q) q