turn proofs for nat into proofs for non-negative ints

Question

I proved some fairly trivial lemma

lemma two_ne_four_mul_any (n:ℕ) : 2 ≠ 2 * 2 * n

Obviously, the same should hold for non-negative Integers, Rationals, Reals, etc.:

lemma two_ne_four_mul_any (z:ℤ) (nonneg: 0 ≤ z): 2 ≠ 2 * 2 * z

In general, if we have p n for some n:nat we should be able to conclude 0 ≤ z → p' z where p' is the "same" as p. However, I don't even see how to formulate this in Lean, let alone how it can be proven.

So, the question is, can this be proven in Lean, and how would one go about it?

Answer 1

can this be proven in Lean

If it's correct mathematics, it can be proven in Lean. You'll need to give the second lemma a different name from the first though.

import tactic

lemma two_ne_four_mul_any (n:ℕ) : 2 ≠ 2 * 2 * n := sorry

lemma two_ne_four_mul_any' (z:ℤ) (nonneg: 0 ≤ z) : 2 ≠ 2 * 2 * z :=
begin
  -- get the natural
  rcases int.eq_coe_of_zero_le nonneg with ⟨n, rfl⟩,
  -- apply the lemma for naturals
  apply_mod_cast (two_ne_four_mul_any n)
end

You have to be a bit careful here -- for example subtraction on naturals and integers can produce different results (e.g. 2-3=0 in the naturals and it's of course -1 in the integers, so if p n := n - 3 = 0 is a statement about naturals then p 2 is true but the naive "same" statement isn't true for integers). The cast tactics know what is true and what is not though.