by_contra' is a tactic for proving propositions by contradiction.
It is similar to
by_contra except that it also uses
push_neg to normalize negations.
If the target of the main goal is a proposition
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.
¬ p will be negation normalized using
¬ a < b will be changed to
b ≤ a.
by_contra' h : q will normalize negations in
¬ p, normalize negations in
and then check that the two normalized forms are equal.
The resulting hypothesis is the pre-normalized form,
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
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 ```