∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] {a b c w : Polynomial k} {hw : w ≠ 0},
  w = a.wronskian b →
    a ≠ 0 →
      b ≠ 0 →
        c ≠ 0 →
          EuclideanDomain.divRadical (a * b * c) ∣ w →
            c.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree