Dear all,

I’d like to be able to write

```
Unset Printing Notations.
Compute (1 <= 2 <= 3 <= 4 <= 5)
```

and have that result in

```
le 1 2 /\ le 2 3 /\ le 3 4 /\ le 4 5
```

Coq ships with a built-in notation `a <= b <= c`

, but I’d like that for arbitrary chain lengths. (I’m not actually interested in the case for `le`

, but for another relation, which shouldn’t make a difference for the approach.)

Any hints or ideas how to implement such a notation?

If that doesn’t work, I’m also okay with something like `chain 1 <= 2 <= 3 <= 4 endchain`

, i.e. explicit begin and end markers.

Many thanks in advance!

Yannick