If the target of the main goal is a proposition p, by_contra' reduces the goal to proving false using the additional hypothesis h : ¬ p. by_contra' h can be used to name the hypothesis h : ¬ p. The hypothesis ¬ p will be negation normalized using push_neg. For instance, ¬ a < b will be changed to b ≤ a. by_contra' h : q will normalize negations in ¬ 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 (tactic.interactive.by_contra).

Examples:

example : 1 < 2 :=
begin
  by_contra' h,
  -- h : 2 ≤ 1 ⊢ false
end

example : 1 < 2 :=
begin
  by_contra' h : ¬ 1 < 2,
  -- h : ¬ 1 < 2 ⊢ false
end
```