In ssrnat, I saw:

```
From mathcomp Require Import all_ssreflect.
Check leq_trans. (* forall n m p : nat, m <= n -> n <= p -> m <= p *)
Check ltn_trans.(* forall n m p : nat, m < n -> n < p -> m < p *)
Check leq_ltn_trans. (* forall n m p : nat, m <= n -> n < p -> m < p *)
```

but I didn't see:

```
Check ltn_leq_trans. (* forall n m p: nat, m <n -> n <= p -> m < p *)
```

there are other combinations of `<=`

and `<`

missing, but I think using `ltnW: forall m n: nat, m <n -> m <= n`

makes them useless, while for `ltn_leq_trans`

, I don't think that's the case.

That's just an instance of `leq_trans`

due to the way `ltn`

is defined:

```
Goal forall n m p: nat, m <n -> n <= p -> m < p.
Proof. by move=> n m p; apply: leq_trans. Qed.
```

Hmmm... and that same proof doesn't work for `leq_ltn_trans`

?

Ah, no because the `S`

doesn't apply to the right variable, if I get it.

(The fact that the strict inequalities all involve large ones on `S m`

makes the proof work.)

I guess that's a case where the special definition of `<`

for type `nat`

has an impact on proofs.

@Cyril Cohen Isn't that precisely an example what you mentioned this morning about adding structure on `nat`

possibly giving issues because there are special hand-written (hence tight) things which will be replaced by something more automatic and hence looser?

Last updated: Jul 23 2024 at 20:01 UTC