apply eq_of_div_mod_two_eq
case right
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ m + n = m ^^^ n
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2

case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2