Given a goal like:

```
Goal
([set tt] :&: [set tt] != set0).
Proof.
```

How can one show this to be correct?

Couldn't figure out how to properly get rid of `:&:`

.

Okay got rid of `:&:`

with `setIid`

. Now stuck on `[set tt] != set0`

..

You can turn this into `~ [set tt] == set0`

with `negP`

, or into `~ [set tt] = set0`

with `eqP`

.

I guess this might be the most efficient way to conclude:

https://github.com/math-comp/math-comp/blob/14411700e3fad6297ccb682ad5a7955ff8202b08/mathcomp/ssreflect/finset.v#L736C1-L737C51

Last updated: Jul 25 2024 at 16:02 UTC