feat(set_theory/surreal/dyadic): tweak API + golf (#14649)
This PR does the following changes:
- Get rid of `pgame.half`, as it's def-eq to `pow_half 1`, which has strictly more API.
- Fix the docstring on `pow_half`, which incorrectly stated `pow_half 0 = 0`.
- Remove `simp` from some type equality lemmas.
- Remove the redundant theorems `pow_half_move_left'` and `pow_half_move_right'`.
- Add instances for left and right moves of `pow_half`.
- Rename `zero_lt_pow_half` to `pow_half_pos`.
- Prove `pow_half_le_one` and `pow_half_succ_lt_one`.
- Make arguments explicit throughout.
- Golf proofs throughout.
