∀ {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (c : AddCon M) (f : M →+ P)
  (H : c ≤ AddCon.ker f) (m n : M), AddCon.liftOn (↑m + ↑n) ⇑f ⋯ = AddCon.liftOn ↑m ⇑f ⋯ + AddCon.liftOn ↑n ⇑f ⋯