∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} {x y : M}
  (a : AddConGen.Rel r x y), AddConGen.Rel.below a → motive x y a → AddConGen.Rel.below ⋯