non_meta_rec_fn.lean:3:36: error: failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r true (@has_well_founded_of_has_sizeof true (default_has_sizeof true))
Possible solutions: 
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
invalid apply tactic, failed to unify
  0 < 0
with
  ?m_1 < ?m_1 + ?m_2
state:
_x : true
⊢ 0 < 0
state:
⊢ false
