Refactoring positive integers

[malarbol]

Resolves #1043.

[fredrik-bakke]

I quite like your organization of the concepts into their own files + a file about the relations between them. But if I didn't misunderstand @EgbertRijke rather wanted one file for all 5? Maybe he can comment on that.

[fredrik-bakke]

Your work looks pretty good so far by the way!

[fredrik-bakke]

In the library, I believe "inequality" is the name we use for the standard ordering on integers and so on. We shouldn't introduce "standard inequality" as an extra term for the same thing.

[malarbol]

In the library, I believe "inequality" is the name we use for the standard ordering on integers and so on. We shouldn't introduce "standard inequality" as an extra term for the same thing.

Ok. I chose inequality over order(ing) to stick with the names of the files ; maybe this was an error and I should have kept a bit of both? And I just stuck standard in a few places because of your comment on the many orderings of ℤ but we can drop them if you prefer.

[fredrik-bakke]

In the library, I believe "inequality" is the name we use for the standard ordering on integers and so on. We shouldn't introduce "standard inequality" as an extra term for the same thing.

Ok. I chose inequality over order(ing) to stick with the names of the files ; maybe this was an error and I should have kept a bit of both? And I just stuck standard in a few places because of your comment on the many orderings of ℤ but we can drop them if you prefer.

I think your choice is very sensible, and I can't see why it is a mistake. It seemed rather arbitrary how the prose kept switching between the two terms before.

[fredrik-bakke]

I like the current version of things, so I think this PR should be merged after my final suggestions have been implemented

[malarbol]

It seemed rather arbitrary how the prose kept switching between the two terms before.

well, each contributor will have its own prose and preferred terms so I guess this is bound to happen somehow. But it does give a kind of "organic" touch. As a reader, it's nice to feel that this was written by humans and that it's not just a juxtaposition of automatically derived proofs and generated text.

I like the current version of things, so I think this PR should be merged after my final suggestions have been implemented

thx. I also quite liked how it all turned out. Thank you again for all your time and dedication.

[fredrik-bakke]

Thank you!

If you don't mind, may I keep myself as co-author of this contribution? Reviewers are automatically added as co-authors when you accept one of their suggestions, but we have a policy that we do not preserve co-authorship status in these cases unless the submitter agrees to it. Normally I wouldn't even ask, but given that we've worked so closely on this one it seems fitting to keep my name on it. I do not mean to take any credit away from you though, you definitely deserve most of it for your hard work!

[malarbol]

If you don't mind, may I keep myself as co-author of this contribution?

Of course! I wouldn't have it any other way. I may have written most of the new code but I definitely consider we worked together on this. (and this goes for any future collaborations; I trust your judgment on your level of contribution).

[fredrik-bakke]

Merged!