∀ {R : Type u_1} {G : Type u_2} [inst : CommSemiring R] [inst_1 : Group G] [inst_2 : MulAction G R] (x : G) (y z : R)
  (motive : IsCoprime (x • y) z → Prop) (x_1 : IsCoprime (x • y) z),
  (∀ (a b : R) (h : a * x • y + b * z = 1), motive ⋯) → motive x_1