theorem Char.le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x

instance Char.instLawfulOrd : Std.LawfulOrd Char

@[simp]

theorem Char.toNat_val (c : Char) : c.val.toNat = c.toNat

@[simp]

theorem Char.toNat_ofNatAux {n : Nat} (h : n.isValidChar) : (ofNatAux n h).toNat = n

theorem Char.toNat_ofNat (n : Nat) : (ofNat n).toNat = if n.isValidChar then n else 0