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: Apr 17 2024 at 23:01 UTC