Cast with apply

Stream: new members

[Bhavik Mehta]

I'm trying to use modeq.dvd_of_modeq in the following, and I think it's failing to unify because of the casts? How could I make this work?

invalid apply tactic, failed to unify
  a - 1 ∣ a ^ n - 1
with
  ↑?m_1 ∣ ↑?m_2 - ↑?m_3
state:
a n : ℕ,
ha : 2 ≤ a
⊢ a - 1 ∣ a ^ n - 1

[Chris Hughes]

The substraction in the statement of the theorem is natural number subtraction, which returns a natural number, and defaults to zero when the answer should be negative. So, for example 2 - 3 = 0.

There are a couple of ways around this. The easiest is to make a an integer.

[Chris Hughes]

The other way is to rw [← int.coe_nat_dvd, int.coe_nat_sub, int.coe_nat_sub] and prove that because 2 ≤ a, a - 1 gives the same answer when done using integer subtraction.

[Kevin Buzzard]

(typo 2 - 3 = 0)

[Bhavik Mehta]

Thanks for these - I'd rather not make a an integer since this is a lemma I need for a larger theorem

[Bhavik Mehta]

I can't seem to get the other way to work - the int.coe_nat_sub looks like it's getting applied to both terms, and I only want to apply it on the right