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

Proof finished

Before

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

contradiction.

After

Proof finished

Resources

Reference Documentation

---