∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {a : R} (r : Polynomial R),
  Polynomial.rootMultiplicity a f = Polynomial.rootMultiplicity a r + Polynomial.rootMultiplicity a f + Nat.succ 0 →
    False