not_def

Stream: Is there code for X?

[Kevin Buzzard]

Do we not have

example : ¬ P ↔ (P → false) := imp_false.symm

?
I was preparing teaching materials for...erm...tomorrow, and was expecting to be able to show students how to "simplify" ¬ P to P → false by rewriting, but imp_false goes the other way :-/

[Eric Wieser]

As I mentioned in another thread, not is missing its equation lemmas, so the standard rw not approach doesn't work here either...

[Yury G. Kudryashov]

Should we move the definition of eq up?

[Eric Wieser]

Can we just insert the equation lemma manually? There's a test showing how to do that.