case zero => calc
  n &&& 2^0 - 1 = n &&& 0 := rfl
  _             = 0 := Nat.land_zero n
  _             = n % 1 := n.mod_one.symm
  _             = n % 2^0 := rfl
n : Nat
⊢ n &&& 2 ^ zero - 1 = n % 2 ^ zero
no goals