CCONTR_TAC
Tactic.CCONTR_TAC : tactic
Assumes the negation of the conclusion of a goal.
Given a goal A ?- t, CCONTR_TAC makes a new goal which is to prove
F by assuming also the negation of the conclusion t.
A ?- t
==========
A, -t ?- F
Failure
Never fails
See also
Tactic.CHECK_ASSUME_TAC,
Thm.CCONTR, Drule.CONTRAPOS,
Thm.NOT_ELIM