Hopf problem: hurewicz · second hurewicz

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.SecondHurewicz.SimplyConnected.subdivision_eq_sub_of_eq_add {A : Type u_1} [AddGroup A] {a b c d : A} (h : a = b + c) (hc : c = -d) : a = b - d