discriminate

discriminate solves goals that are trivial inequalities (something of the form x <> y). This tactic will fail if the goal is not an inequality or is non-trivial.

Syntax

(* Simple usage *)
discriminate.

Examples

Before

-------------------------
1/1
1 <> 2

discriminate.

After

Proof finished

Before

-------------------------
1/1
"hello" <> "world"

discriminate.

After

Proof finished

Resources

Reference Documentation

---