Theorem: Nat.eq_of_div_mod_two_eq (Algdata/Data/Nat/Bits.lean)

State before:
m n : Nat
hdiv : m / 2 = n / 2
hmod : m % 2 = n % 2
⊢ 2 * (m / 2) + m % 2 = 2 * (n / 2) + n % 2
Tactic:
rw [hdiv, hmod]
State after:
no goals