I have quite a few lemmas on Z, e.g. a complete set of interval arithmetic lemmas for known signs and unknown signs for multiplication and division e.g.:

```
Lemma Z_mult_bounds: forall a b amin amax bmin bmax : Z,
amin <= a <= amax ->
bmin <= b <= bmax ->
Z_min4 (amin*bmin) (amin*bmax) (amax*bmin) (amax*bmax) <= a*b <= Z_max4 (amin*bmin) (amin*bmax) (amax*bmin) (amax*bmax).
Lemma Z_div_bounds_nonneg_neg: forall a b amin amax bmin bmax : Z,
0 <= amin ->
bmax < 0 ->
amin <= a <= amax ->
bmin <= b <= bmax ->
(amax + bmax - bmin) / bmax <= a/b <= (amin + bmin - bmax) / bmin.
```

or things like:

```
Lemma Z_div_den_opp_pos: forall a b : Z,
b > 0 ->
a / - b = - ((a + b - 1)/ b).
Lemma Z_div_den_opp_neg: forall a b : Z,
b < 0 ->
a / - b = - ((a + b + 1)/ b).
```

(the standard library has lemmas for `a/-b`

but one needs to know if `a mod b`

is zero, while for mine one needs to know the sign of b). I find such stuff surprisingly tedious to prove, even with lia.

I wonder if I should put this into the standard library, or if this is too specific. Is there something like a "standard library call" as there is a "Coq call" where such things are discussed?

Is there something like a "standard library call" as there is a "Coq call" where such things are discussed?

There could be. @Emilio Jesús Gallego Arias has proposed the idea of having regular thematic WG. See https://github.com/coq/coq/wiki/Topic-Working-Groups. You could launch one with interested stakeholders.

I tried 2x to create a new Wiki page for a new group but either I am doing something silly or it is broken - if I go to the preview for a new page it says "preview generation failed" and when I save the page I get an error. I really do only very simple markdown. Any ideas? I am using Safari on macOS btw.

I think github is bugging, I tried to subscribe to an issue (on a non coq repo) and github ignored me

I tried starring a repo and github said "you are not allowed at this time"

Thanks - I will try again tomorrow then.

looks like it works now

Last updated: Oct 16 2021 at 07:02 UTC