DecidableLE のインスタンスをタクティクで作ってはいけない

example {a b : MyInt} (h : ∃ k : MyNat, a + (k + 1) = b) : a < b := by
  notation_simp
  constructor
  case left =>
    obtain ⟨k, hk⟩ := h
    use k + 1
    assumption
  case right =>
    intro ⟨s, hs⟩
    obtain ⟨k, h⟩ := h
    rw [← hs] at h
    have : (↑s + ↑k) + (1 : MyInt) = 0 := calc
      _ = (b + ↑s + (↑k + 1)) - b := by abel
      _ = b - b := by rw [h]
      _ = 0 := by abel

    have : 0 > 0 := calc
      _ = (↑s + ↑k) + (1 : MyInt) := by rw [this]
      _ = (1 : MyInt) + ↑s + ↑k := by ac_rfl
      _ ≥ (1 : MyInt) + ↑s := by apply MyInt.le.intro
      _ ≥ (1 : MyInt) := by apply MyInt.le.intro
      /-
      tactic 'decide' failed for proposition
        1 > 0
      since its 'Decidable' instance
        instDecidableLTMyInt 0 1
      did not reduce to 'isTrue' or 'isFalse'.

      After unfolding the instances 'instDecidableAnd', 'instDecidableLEMyInt', 'instDecidableLTMyInt' and 'instDecidablePredMyIntLeOfNat', reduction got stuck at the 'Decidable' instance
        ⋯ ▸ (1 - 0).bpos.decEq true

      Hint: Reduction got stuck on '▸' (Eq.rec), which suggests that one of the 'Decidable' instances is defined using tactics such as 'rw' or 'simp'. To avoid tactics, make use of functions such as 'inferInstanceAs' or 'decidable_of_decidable_of_iff' to alter a proposition.
      -/
      _ > (0 : MyInt) := by decide
    sorry

Start with the Lean example in the issue body and reproduce the failure at the by decide step. Investigate the Decidable instances named in the error and determine the intended non-tactic construction; the example should compile without the shown sorry or reduction failure.