Theorem AnalyticOnNhd.codiscrete_setOf_order_eq_zero_or_top

refactor: use a junk value for the analytic order of a non-analytic function (#22974) …

feat: characterize level sets of the order for analytic/meromorphic functions (#22292) …