m n : ℕ
h₁ : bit1 (m * (n / m) + n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
m n : ℕ
⊢ bit1 n % bit0 m = bit1 (n % m)
have h₁ := congr_arg bit1 (Nat.div_add_mod n m)
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
m n : ℕ
h₁ : bit1 (m * (n / m) + n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
rw [bit1_add, bit0_eq_two_mul, ← mul_assoc, ← bit0_eq_two_mul] at h₁
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (bit1 n / bit0 m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
have h₂ := Nat.div_add_mod (bit1 n) (bit0 m)
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (n / m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (bit1 n / bit0 m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
rw [bit1_div_bit0] at h₂
no goals
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (n / m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
exact add_left_cancel (h₂.trans h₁.symm)