If the target of the main goal is a proposition `p`

,
`by_contra'`

reduces the goal to proving `False`

using the additional hypothesis `this : ¬ p¬ p`

.
`by_contra' h`

can be used to name the hypothesis `h : ¬ p¬ p`

.
The hypothesis `¬ p¬ p`

will be negation normalized using `push_neg`

.
For instance, `¬ a < b¬ a < b`

will be changed to `b ≤ a≤ a`

.
`by_contra' h : q`

will normalize negations in `¬ p¬ p`

, normalize negations in `q`

,
and then check that the two normalized forms are equal.
The resulting hypothesis is the pre-normalized form, `q`

.
If the name `h`

is not explicitly provided, then `this`

will be used as name.
This tactic uses classical reasoning.
It is a variant on the tactic `by_contra`

.
Examples:

```
example : 1 < 2 := by
by_contra' h
-- h : 2 ≤ 1 ⊢ False
example : 1 < 2 := by
by_contra' h : ¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
≤ 1 ⊢ False
example : 1 < 2 := by
by_contra' h : ¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
⊢ False
example : 1 < 2 := by
by_contra' h : ¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
¬ 1 < 2 ⊢ False
⊢ False
```

## Equations

- One or more equations did not get rendered due to their size.