c : Char
h : isValidCharNat (toNat c)
⊢ ofNatAux (toNat c) h = c
c : Char
h : isValidCharNat (toNat c)
⊢ ofNat (toNat c) = c
rw [Char.ofNat, dif_pos h]
no goals
c : Char
h : isValidCharNat (toNat c)
⊢ ofNatAux (toNat c) h = c
rfl