## Stream: new members

### Topic: How to use dvd_refl

#### Shadman Sakib (Jun 06 2021 at 19:34):

How do I use dvd_refl to show a | a as hyp?

#### Shadman Sakib (Jun 06 2021 at 19:39):

Or just to use it as a fact

#### Yakov Pechersky (Jun 06 2021 at 19:47):

have my_hyp : a ∣ a := dvd_refl a

Ahh, Thank you!

#### Yakov Pechersky (Jun 06 2021 at 19:50):

You don't have to do the : a ∣ a part, you can just do have my_hyp := dvd_refl a

#### Shadman Sakib (Jun 06 2021 at 19:54):

Okay, how can I combine this hypothesis with an earlier one ( a | b) to show gcd(a b) = a?

#### Shadman Sakib (Jun 06 2021 at 19:55):

im assuming dvd_gcd_iff but I'm not sure how to implement it

#### Shadman Sakib (Jun 06 2021 at 19:56):

In other words, is there a way to say, well since a|a and a|b, then gcd(a b) = a

#### Yakov Pechersky (Jun 06 2021 at 19:57):

Have you done the Natural Numbers Game?

No

#### Shadman Sakib (Jun 06 2021 at 19:58):

I am doing the tutorial

#### Yakov Pechersky (Jun 06 2021 at 20:00):

I think the NNG is very good at getting used to the way that lemmas are introduced, applied, and found. That might be good before the tutorial, if you'd like. The answer to your question re gcd is docs#nat.gcd_eq_left_iff_dvd

#### Shadman Sakib (Jun 06 2021 at 20:01):

So how would i apply this lemma?

#### Yakov Pechersky (Jun 06 2021 at 20:03):

It's hard for me to say what "apply" means in your context without seeing more of your tactic state

#### Patrick Massot (Jun 06 2021 at 20:09):

In the context of this tutorial, the exercise is a bit tricky on purpose. The constraints are to use a very limited set of lemmas.

#### Patrick Massot (Jun 06 2021 at 20:10):

Recall the first life of this series of exercises was in actual teaching where you need almost every file to end with a more challenging exercise to keep the good students busy while the slower ones work through the main exercises.

Last updated: Dec 20 2023 at 11:08 UTC