[Merged by Bors] - feat: gcd and coprime sub

[mo271]

---

[mo271]

I'm not super sure about the naming.
I also considered if this was a good addition to std, but I think this is the better place for it.

[adomani]

What is the reason to introduce the lemmas that deal with subtraction and then switch the inputs to gcd? I would have thought that there should be the simp lemma that removes the subtraction, but I am not sure about also swapping the arguments.

[mo271]

What is the reason to introduce the lemmas that deal with subtraction and then switch the inputs to gcd? I would have thought that there should be the simp lemma that removes the subtraction, but I am not sure about also swapping the arguments.

The reason I added both versions was to try to be in sync with what is done for the add lemmas above. Let's see:

1: gcd m (n + m) = gcd m n
2: gcd (m + n) n = gcd m n
3: gcd (m + n) m = gcd n m
4: gcd m (m + n) = gcd m n

exchanging m and n on the righthand side to always be gcd m n, we then have

1: gcd m (n + m) 
2: gcd (m + n) n
3: gcd (n + m) n
4: gcd m (m + n) 

by analogy we replace the + by the -

1: gcd m (n - m) 
2: gcd (m - n) n
3: gcd (n - m) n
4: gcd m (m - n) 

I suppose you are right, there are only 4 lemmas needed. That's what I did now...

[adomani]

Yes, my reasoning was: the argument that does not have add/sub stays what it is and does not swap places with the other. The simp lemma just undoes one operation in one coordinate, but does not also swap coordinates.

Of course, e.g. in the Euclidean algorithm, you alternate subtracting and swapping, but I think that the simp lemma should not be trying to do that.

[adomani]

I personally find the naming strange, but it seems to be consistent with the add versions. LGTM!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build

[ADedecker]

bors retry

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style