dumb question on ring tactic

Stream: new members

[Daniel Oberski]

I have a very n00b question. Sorry if it is somewhere in a manual or book I should have read....

I thought to do a few simple problems from our number theory course but got stuck on problem 2. The goal is solved when I replace every ℕ with ℝ, but obviously that is not what i need! The ring tactic does not seem to like the /2 bit, but I am not sure what to do about it. Any help to a complete newbie (even if it is telling me which manual to read to understand what is going on) is greatly appreciated!

def triangular (n : ℕ) :=  ∃ (k : ℕ), n = k  * (k + 1) / 2

-- Exercise 2.2(a)
example (n : ℕ) (h: triangular n) : triangular (9*n + 1) :=
begin
  cases h with k h,
  rw h,
  fconstructor,
  use 3*k + 1,
  -- ring does not close with ℕ or ℤ, only with ℝ. Not sure how to fix it.
  ring,
end

[Yaël Dillies]

Did you know that 3/2 = 1? Natural and integer division round down, so ring doesn't support them. You should use rat if you talk about division.

[Daniel Oberski]

I see, thanks Yaël!
I found this way around the problem:

def triangular (n : ℕ) :=  ∃ (k : ℕ), 2 * n = k  * (k + 1)

-- Exercise 2.2(a)
example (n : ℕ) (h: triangular n) : triangular (9*n + 1) :=
begin
  cases h with k h,
  use 3*k + 1,
  linarith,
end