I'm having some troubles doing contra like tactic for classical_sets.

I'm trying to prove `Y <> X /\ X `<=` Y -> X `<=` Y /\ (exists2 a : T, Y a & ~ X a)`

So far I can prove that the goal can be rewritten as `Y `\` X != set0`

. I'd like to use setD_eq0 by doing contraposition reasonning. Unfortunatly I don't know how to do : apparently contraPN is not available in classical_sets.v ("The reference contraPN was not found in the current environment.") despite all_ssreflect being imported.

@vlj `contraPN`

was added recently, maybe your math-comp version is too old

if so just copy to an aux library that you can remove when upgrading

ho ok didn't know

is there a double negation in boolp ?

err contrapT

vlj said:

is there a double negation in boolp ?

`notK`

?

(double negation elimination)

thanks ! will try to see if it simplify the proof

actually contra_not_neq is actually better fitter.

Last updated: Feb 09 2023 at 02:02 UTC