| letRecMissingAnnotation.lean:4:6-4:34: error: failed to prove termination, possible solutions: | |
| - Use `have`-expressions to prove the remaining goals | |
| - Use `termination_by` to specify a different well-founded relation | |
| - Use `decreasing_by` to specify your own tactic for discharging this kind of goal | |
| as : Array Nat | |
| i s : Nat | |
| h : i < Array.size as | |
| ⊢ Array.size as - (i + 2) < Array.size as - i |