Hello, I would like to convert

```
x \in `]0, 1[
```

into

`0 < x < 1`

because the latter can be used by `lra`

. How do I do that?

Does `rewrite in_itv`

works?

I added it as my TODO on the Algebra Tactics side. It's not clear to me how to do that, but it should be doable. https://github.com/math-comp/algebra-tactics/issues/73

The solution proposed by @Pierre Roux is good, but I am disappointed that search did not help me find it.

Yves Bertot has marked this topic as resolved.

Last updated: Jul 23 2024 at 20:01 UTC