∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M → N),
  Function.Bijective f →
    ∀ (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : N → N → Prop),
      AddCon.comap f H (addConGen rel) = addConGen fun x y => rel (f x) (f y)