α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : Nat.beq n✝¹ n✝ = false
⊢ ¬n✝¹ = n✝
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : Nat.beq n✝¹ n✝ = false
⊢ ¬↑n✝¹ = ↑n✝
simp
no goals
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : Nat.beq n✝¹ n✝ = false
⊢ ¬n✝¹ = n✝
exact Nat.ne_of_beq_eq_false h