∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  (r₁ r₂ : S)
  (motive :
    { k //
        Polynomial.eval (r₁ + (r₂ - r₁)) (Polynomial.map (algebraMap R S) P) =
          Polynomial.eval r₁ (Polynomial.map (algebraMap R S) P) +
              Polynomial.eval r₁ (Polynomial.derivative (Polynomial.map (algebraMap R S) P)) * (r₂ - r₁) +
            k * (r₂ - r₁) ^ 2 } →
      Prop)
  (x :
    { k //
      Polynomial.eval (r₁ + (r₂ - r₁)) (Polynomial.map (algebraMap R S) P) =
        Polynomial.eval r₁ (Polynomial.map (algebraMap R S) P) +
            Polynomial.eval r₁ (Polynomial.derivative (Polynomial.map (algebraMap R S) P)) * (r₂ - r₁) +
          k * (r₂ - r₁) ^ 2 }),
  (∀ (u : S)
      (hu :
        Polynomial.eval (r₁ + (r₂ - r₁)) (Polynomial.map (algebraMap R S) P) =
          Polynomial.eval r₁ (Polynomial.map (algebraMap R S) P) +
              Polynomial.eval r₁ (Polynomial.derivative (Polynomial.map (algebraMap R S) P)) * (r₂ - r₁) +
            u * (r₂ - r₁) ^ 2),
      motive ⟨u, hu⟩) →
    motive x