What tactic should I use to derive a contradiction from an absurd equality?

Question

Let's say that I have H: 0 = 1 in scope. How can I use this to conclude False?

Answer 1

You should use the tactic discriminate.