How to use dvd_refl

Stream: new members

[Shadman Sakib]

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

[Shadman Sakib]

Or just to use it as a fact

[Yakov Pechersky]

have my_hyp : a ∣ a := dvd_refl a

[Shadman Sakib]

Ahh, Thank you!

[Yakov Pechersky]

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

[Shadman Sakib]

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

[Shadman Sakib]

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

[Shadman Sakib]

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

[Yakov Pechersky]

Have you done the Natural Numbers Game?

[Shadman Sakib]

No

[Shadman Sakib]

I am doing the tutorial

[Yakov Pechersky]

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]

So how would i apply this lemma?

[Yakov Pechersky]

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

[Patrick Massot]

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]

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.