How to rewrite (0 : nat) as bot, or conversely

Stream: new members

[Antoine Chambert-Loir]

Yesterday, I had to change 0 : nat into ⊥ : nat in some equality h : … = 0.
In the absence of nat.zero_eq_bot, there does not seem to be a preferred way to do that.
I had entered change : _ = ⊥, but I finally decided I prefered adding have : (0 : nat) = ⊥ := rfl.
Which one is preferable?

Below is a MWE where @María Inés de Frutos Fernández and I use this.

import data.mv_polynomial.variables

variables {σ : Type*} {R : Type*} [comm_semiring R]

namespace mv_polynomial

lemma total_degree_eq_zero_iff (p : mv_polynomial σ R) :
  p.total_degree = 0
  ↔ ∀ (m : σ →₀ ℕ) (hm : m ∈ p.support) (x : σ), m x = 0 :=
begin
  have nat_zero_eq_bot : (0 : ℕ) = ⊥ := rfl,
  rw [nat_zero_eq_bot, total_degree, finset.sup_eq_bot_iff, ← nat_zero_eq_bot],
  apply forall_congr,
  intro a,
  apply forall_congr,
  intro ha,
  simp only [finsupp.sum, finset.sum_eq_zero_iff, finsupp.mem_support_iff, not_imp_self],
end

end mv_polynomial

[Yaël Dillies]

docs#bot_eq_zero

[Antoine Chambert-Loir]

Thanks! I don't understand how I didn't find it - probably because I was looking to zero_eq_bot…

[Adam Topaz]

Another option is to introduce the term on the fly and rewrite like this rw (show 0 = \bot, from rfl)