∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (c : AddCon M) (f : N →+ M)
  (hf : Function.Surjective ⇑f),
  c.comapQuotientEquivOfSurj f hf = (AddCon.congr ⋯).trans (AddCon.quotientKerEquivOfSurjective (c.mk'.comp f) ⋯)