Hello, I am a beginner to Coq (and this is my first time posting here) and I tried to prove that for two integers each larger than zero, their sum is also larger than zero. I am using jsCoq (0.16.0), which is running Coq 8.16.0 at the time of writing this.

(I am aware of the existence of nat and the “positive” type, especially when dealing with the QArith module, but for now I am interested in the ZArith module with its Z type.)

I used the additivity and transitivity properties of the total order of integers:

- additivity: for all a, b, c \in \mathbb{Z}, if a < b then a + c < b + c
- transitivity: for all a, b, c \in \mathbb{Z}, if a < b and b < c then a < c

I tried two approaches, which resulted in two slightly different proofs. My first proof involves transforming all “greater than” into “less than” before applying any lemmas, while my second proof directly applies existing “greater than” lemmas. Here is my code:

```
Require Import ZArith.
Lemma firstproof : forall z1 z2 : Z, (z1 > 0)%Z /\ (z2 > 0)%Z -> ( (z1 + z2)%Z > 0 )%Z.
Proof.
intros z1 z2.
intro H.
destruct H as [H1 H2].
(* flip "greater than" into "less than" *)
apply Z.gt_lt in H1.
apply Z.gt_lt in H2.
(* additivity *)
apply Zplus_lt_compat_r with (n := 0%Z) (m := z1) (p := z2) in H1.
simpl in H1.
(* transitivity *)
pose proof Z.lt_trans as H3.
specialize H3 with (n := 0%Z) (m := z2) (p := (z1 + z2)%Z).
specialize (H3 H2 H1) as H3. (* modus ponens, twice *)
(* flip H3 back into greater than, then finish the proof *)
apply Z.lt_gt in H3.
apply H3.
Qed.
Lemma secondproof : forall z1 z2 : Z, (z1 > 0)%Z /\ (z2 > 0)%Z -> ( (z1 + z2)%Z > 0 )%Z.
Proof.
intros z1 z2.
intro H.
destruct H as [H1 H2].
(* additivity *)
apply Zplus_gt_compat_r with (n := z1) (m := 0%Z) (p := z2) in H1.
simpl in H1.
(* transitivity *)
pose proof Zgt_trans as H3.
specialize H3 with (n := (z1 + z2)%Z) (m := z2) (p := 0%Z).
specialize (H3 H1 H2) as H3. (* modus ponens, twice *)
(* H3 is what we wanted to prove *)
apply H3.
Qed.
```

I used the `Search`

keyword a few times when developing those proofs, and I got a bit confused with some inconsistency in the names of the lemmas that I applied (or posed as new hypotheses). Namely:

- The names of some lemmas I applied start with
`Z.`

, and some others start with`Z`

without the period (not even an underscore replacing the period). - For transitivity, there is
`Z.lt_trans`

for when we have a < b etc (as I stated above), but`Zgt_trans`

for when we have a > b. Meanwhile, neither`Zlt_trans`

nor`Z.gt_trans`

exists (the`Check`

command says`The reference (name) was not found in the current environment.`

).

Frustrated about the second point, I tried browsing the Coq repository on GitHub, specifically the coq/theories/ZArith directory, to look for the original vernacular source code of these lemmas, in the hopes that I might be able to contribute and make the naming more consistent (perhaps by adding `Definition Z.gt_trans := Zgt_trans`

or something). I ended up having trouble looking for them…

So instead, I decided to use the `Locate`

command back in jsCoq. Here’s what I got:

`Locate Z.gt_lt`

gives`Constant Coq.ZArith.BinInt.Z.gt_lt`

`Locate Z.lt_gt`

gives`Constant Coq.ZArith.BinInt.Z.lt_gt`

`Locate Zplus_lt_compat_r`

gives`Constant Coq.ZArith.Zorder.Zplus_lt_compat_r`

`Locate Zplus_gt_compat_r`

gives`Constant Coq.ZArith.Zorder.Zplus_gt_compat_r`

`Locate Z.lt_trans`

gives`Constant Coq.ZArith.BinInt.Z.lt_trans`

`Locate Zgt_trans`

gives`Constant Coq.ZArith.Zorder.Zgt_trans`

So basically, I’ve been relying on the BinInt and Zorder vernacular files for my proofs.

(Even after knowing that, I still had trouble finding those lemmas in the `BinInt.v`

and `Zorder.v`

files on the GitHub repository. Maybe something happened in the latest 8.17 update of Coq?)

However, I noticed that in the GitHub repository as it is now, **Zorder.v is stated to be deprecated** in a comment inside the file itself (near the top):

```
(** THIS FILE IS DEPRECATED.
It is now almost entirely made of compatibility formulations
for results already present in BinInt.Z. *)
```

This deprecation message also exists in some other files within the same ZArith directory.

My questions:

- With
`Zorder.v`

being deprecated, does it actually mean that the use of all lemmas located in Zorder is also deprecated (therefore the use of`Zplus_lt_compat_r`

,`Zplus_gt_compat_r`

, and`Zgt_trans`

is all deprecated)? - If #1 is true, what are their replacements (which I suppose are in BinInt)? Is there a good reference to see all the deprecated lemmas and their replacements, or at least to see the currently supported (not deprecated) lemmas, or something?
- When dealing with inequalities, it seems that “less than” lemmas are more supported than “greater than” lemmas (I sometimes use the
`Search`

feature with > and often found less results than with <). Is this intended, or can I contribute on GitHub to “close the gap” by adding the “greater than” counterparts of existing lemmas? - I have trouble memorizing all of these lemma names, and rely on the
`Search`

feature embarrassingly often. Is there a particular naming convention being used, or is it all a huge mess as it is today (given the inconsistencies)?

I admit, most of the details of what I was trying to prove isn’t really important for what I’m asking. I apologize that I wasn’t able to provide a minimal working example, in fear that the motivations for asking those questions would become unclear.