How does `decreasing_tactic` work?

Stream: new members

[Bbbbbbbbba]

Why do I have to single out hdec.right for Lean to automatically prove termination, but not hdec_left?

import Mathlib

lemma dec_lemma {b : ℕ+} {x : ℕ} : 0 < x → Nat.log b x < x ∧ x - b ^ Nat.log b x * (x / b ^ Nat.log b x) < x := sorry

def nat_to_nat (b : ℕ+) (b1 : ℕ+) (x : ℕ) :=
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    have hdec : e < x ∧ x - b ^ e * n < x := dec_lemma h
    -- have _ := hdec.left  -- This can be commented without problem
    have _ := hdec.right  -- Comment this and Lean fails to prove termination
    b1 ^ (nat_to_nat b b1 e) * n + (nat_to_nat b b1 (x - b ^ e * n : ℕ))
  else 0
  termination_by x