∀ {R : Type u_1} [inst : Ring R] (motive : Polynomial R → (x : Polynomial R) → x.Monic → Prop) (x x_1 : Polynomial R)
  (x_2 : x_1.Monic), (∀ (p q : Polynomial R) (hq : q.Monic), motive p q hq) → motive x x_1 x_2