∀ {R : Type u} [inst : Semiring R] {M : Polynomial R → Sort u_1} (p : Polynomial R) (M0 : M 0)
  (MC : (p : Polynomial R) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + Polynomial.C a))
  (MX : (p : Polynomial R) → p ≠ 0 → M p → M (p * Polynomial.X)),
  p.recOnHorner M0 MC MX =
    if hp : p = 0 then ⋯ ▸ M0
    else
      have wf := ⋯;
      ⋯.mpr
        (if hcp0 : p.coeff 0 = 0 then ⋯.mpr (⋯.mpr (⋯.mpr (MX p.divX ⋯ (p.divX.recOnHorner M0 MC MX))))
        else
          MC (p.divX * Polynomial.X) (p.coeff 0) ⋯ hcp0
            (if hpX0 : p.divX = 0 then
              have this := ⋯.mpr (⋯.mpr M0);
              this
            else MX p.divX hpX0 (p.divX.recOnHorner M0 MC MX)))