intro hn hm
case h.right.right
m n : Nat
⊢ n % 2 = 1 → m % 2 = 1 → (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0