CONTRAPOS
Drule.CONTRAPOS : (thm -> thm)
Deduces the contrapositive of an implication.
When applied to a theorem A |- s ==> t, the inference rule CONTRAPOS
returns its contrapositive, A |- ~t ==> ~s.
A |- s ==> t
---------------- CONTRAPOS
A |- ~t ==> ~s
Failure
Fails unless the theorem is an implication.