intro hn hm
case right.right
m n : Nat
⊢ n % 2 = 1 → m % 2 = 1 → decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))