contradiction

contradiction solves goals in which there exist contradictory hypotheses. These contradictions generally take the form of a False hypothesis or a pair of hypotheses that state P and ~ P for some proposition. This tactic will fail if no such contradictions exist.

Syntax

(* Simple usage *)
contradiction.

Examples

Before

H: False
=========================
1/1
False

contradiction.

After

No more goals.

Before

x, y: nat
H: x = y
H0: x <> y
=========================
1/1
x = x + y

contradiction.

After

No more goals.

Resources

Reference Documentation

---