Theorem: Usa2023P2.val_div (Compfiles/Usa2023P2.lean)

State before:
a b : ℝ+
⊢ ↑(a / b) = ↑a / ↑b
Tactic:
rfl
State after:
no goals