`notP` is defined twice

[affeldt-aist]

in contra.v:

https://github.com/math-comp/analysis/blob/61acc8dd2fa007265e5aabcd76cf47f6ee7a812c/classical/contra.v#L272

and in boolp.v:

https://github.com/math-comp/analysis/blob/61acc8dd2fa007265e5aabcd76cf47f6ee7a812c/classical/boolp.v#L686

causing different behaviors according to which module is require imported.

[affeldt-aist]

fyi @t6s

[t6s]

fyi @t6s

the former looks internal to contra, thus not meant to be exported, while the latter looks like a misnomer since it is about double negations

[t6s]

fyi @t6s

the former looks internal to contra, thus meant to be exported, while the latter looks like a misnomer since it is about double negations