# Zulip Chat Archive

## Stream: new members

### Topic: Unable to apply dvd_sub

#### Ben Nale (Aug 11 2020 at 22:39):

I want to show that gcd(a,b) \mid a-b

this is what I typed into lean:

have h3: nat.gcd a b ∣ a - b ,

cases nat.gcd_dvd a b,

apply dvd_sub,

However, I get an error under apply saying that unable to unify m_1 \mid m_2-m_3 even though the goal is in this exact form.

Note that using the exact same technique and div_add I am able to prove the addition version of this lemma.

image.png

#### Kenny Lau (Aug 11 2020 at 22:47):

the typeclasses are different

#### Kenny Lau (Aug 11 2020 at 22:47):

`dvd_sub`

is for commutative rings

#### Kenny Lau (Aug 11 2020 at 22:47):

but `nat`

is only a commutative semiring

#### Kenny Lau (Aug 11 2020 at 22:48):

the subtraction in nat is different

#### Ben Nale (Aug 11 2020 at 22:48):

Oh so I could say (nat.gcd a b : \Z ) \mid (a-b :\Z)

#### Kevin Buzzard (Aug 11 2020 at 22:48):

Yes

#### Kevin Buzzard (Aug 11 2020 at 22:50):

If you type `#check @dvd_sub`

you can see all the type classes required to make the lemma work, and you can see if `nat`

has them by trying to construct them with `apply_instance`

, e.g. `example : comm_ring \N := by apply_instance`

, which of course fails because nat isn't a ring.

#### Ben Nale (Aug 11 2020 at 22:50):

Oh the apply works now. Though using cases on nat.gcd_dvd a b produces to hypotheses with no arrows. But we need arrows

#### Ben Nale (Aug 11 2020 at 22:50):

#### Kevin Buzzard (Aug 11 2020 at 22:51):

the arrow is just the function from nat to int. You might be able to get rid of it with the `norm_cast`

tactic.

#### Ben Nale (Aug 11 2020 at 22:52):

Nice. It works and I get it. Thanks.

#### Ben Nale (Aug 11 2020 at 22:53):

have h3: (nat.gcd a b :ℤ ) ∣ (a - b :ℤ) ,

cases nat.gcd_dvd a b,

apply dvd_sub,

norm_cast,

exact left,

norm_cast,

exact right,

#### Ben Nale (Aug 11 2020 at 22:53):

no goals :)

#### Kenny Lau (Aug 12 2020 at 06:34):

Last updated: May 15 2021 at 23:13 UTC