. have h := I_not_lt r'; rw [←h_full] at h; sorry
case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
no goals