Theorem: isValidChar_UInt32 (Fixtures/Termination/Init/Prelude.lean)

State before:
n : Nat
h✝ : Nat.isValidChar n
h : LT.lt n 55296
⊢ LT.lt 55296 UInt32.size
Tactic:
decide
State after:
no goals

State before:
n : Nat
h✝ : Nat.isValidChar n
left✝ : LT.lt 57343 n
h : LT.lt n 1114112
⊢ LT.lt 1114112 UInt32.size
Tactic:
decide
State after:
no goals