# Zulip Chat Archive

## Stream: new members

### Topic: Cast with apply

#### Bhavik Mehta (Oct 28 2019 at 19:53):

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 (Oct 28 2019 at 19:58):

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 (Oct 28 2019 at 20:02):

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 (Oct 29 2019 at 00:36):

(typo `2 - 3 = 0`

)

#### Bhavik Mehta (Oct 30 2019 at 19:07):

Thanks for these - I'd rather not make `a`

an integer since this is a lemma I need for a larger theorem

#### Bhavik Mehta (Oct 30 2019 at 19:09):

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

Last updated: May 06 2021 at 22:13 UTC