Theorem Ordinal.cof_map_of_isNormal

feat: `cof α = cof β` given a strictly monotonic function `f : α → β` with cofinal range (#36703) …