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

instance instLawfulOrdChar : Batteries.LawfulOrd Char