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: Oct 13 2024 at 01:02 UTC