∀ {M : Type u_1} [inst : Add M] (c : AddCon Mᵃᵒᵖ) {w x y z : M},
  c (AddOpposite.op x) (AddOpposite.op w) →
    c (AddOpposite.op z) (AddOpposite.op y) → c ({ unop' := z } + { unop' := x }) ({ unop' := y } + { unop' := w })