case mk
n✝ m n val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑(bit0 { val := val✝, isLt := isLt✝ }) = bit0 ↑{ val := val✝, isLt := isLt✝ } % n
n✝ m n : ℕ
k : Fin n
⊢ ↑(bit0 k) = bit0 ↑k % n
cases k
no goals
case mk
n✝ m n val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑(bit0 { val := val✝, isLt := isLt✝ }) = bit0 ↑{ val := val✝, isLt := isLt✝ } % n
rfl