I can't find `forall (a b : Z) (d : positive), a=b <-> (a#d)==(b#d).`

; neither can I find `forall (a b z: positive), a*z=b*z <-> a=b`

nor `forall (a b z : Z), z>0 -> a*z=b*z <-> a=b`

which would have been useful writing the first proof myself…am I missing something here? I would have expected to find these in the stdlib?

I proved various assorted Q lemmas when working on reals - unfortunately I didn't have time yet to put them where they belong. You find them in `theories/Reals/Cauchy/QExtra.v`

.

As you can see there, such things are easy to prove by unfolding the definitions of Q arithmetic which brings you to Z arithmetic and then using lia or ring.

An example proof for your first question:

```
Goal forall (a b : Z) (d : positive), a=b <-> (a#d)==(b#d).
intros a b d.
unfold Qeq. cbn. symmetry.
apply Z.mul_cancel_r.
lia.
Qed.
```

And yes, the Q arithmetic in the standard library needs some enhancements.

Much obliged; that's about 25 lines more impressive than my proof! Would it be a bad idea for me to just open PRs for lemmas like these?

I think it would make more sense to make an inventory and a proper plan than spot issues. I actually thought about cleaning up the file I mentioned above and distributing it into the proper places and filling gaps. The QExtra file has lemmas which I needed in some Reals proofs only. If you have a list of lemmas which are missing, that would be a good start. An important question is also how to name the lemmas. I would enjoy a discussion on this topic.

To get the ball rolling! https://github.com/coq/coq/issues/14066

Last updated: Jun 23 2024 at 01:02 UTC