contrapose and push_neg

Stream: general

[Johan Commelin]

@Patrick Massot Thanks a lot for these tactics! They are really nice, and they allow one to reason like a real grown-up mathematician!

[Patrick Massot]

You're welcome! It's purely a product of my undergraduate teaching with Lean. Those tactics are indeed unavoidable if you want Lean proofs to look like real proofs (unfortunately they are far from sufficient).

[Johan Commelin]

Should exfalso take an optional argument?
I can imagine exfalso foo working like exfalso; refine foo.