no goals
m n✝ a b c d n : ℕ
⊢ n % 4 = 3 → n % 2 = 1
simpa [ModEq, show 2 * 2 = 4 by norm_num, show 3 % 4 = 3 by norm_num] using
  @ModEq.of_mul_left 2 n 3 2
no goals
m n✝ a b c d n : ℕ
⊢ 2 * 2 = 4
norm_num
no goals
m n✝ a b c d n : ℕ
⊢ 3 % 4 = 3
norm_num