Lean 4 omega pulls in Classical.choice for ↔ and ∧ goals (and ↔ hypotheses)

Tested on Lean v4.35 core omega with #print axioms. Goals of the form a = 0, a ≤ b ∨ b < a, ¬ b ≤ a, a ≠ b, or an implication between facts gave [propext, Quot.sound]. A goal b = a + b ↔ a = 0, a goal a ≤ 3 ∧ b + 1 ≠ 0, or an ↔ among the hypotheses gave [propext, Classical.choice, Quot.sound]. Splitting by hand is clean: ⟨fun _ => by omega, fun _ => by omega⟩ for ↔ and ⟨by omega, by omega⟩ for ∧. This is why core's Nat.right_eq_add (@[simp high], proved by omega) carries Classical, and why simp closing n + 1 = m + 1-style goals can make a constructive development classical. List.all_eq_false (@[simp], core) is classical as well; for constructive work, prove your own bounded-search lemma by induction with List.range_succ and List.all_cons.