# Contrapose #

The `contrapose`

tactic transforms the goal into its contrapositive when that goal is an
implication.

`contrapose`

turns a goal`P → Q→ Q`

into`¬ Q → ¬ P¬ Q → ¬ P→ ¬ P¬ P`

`contrapose!`

turns a goal`P → Q→ Q`

into`¬ Q → ¬ P¬ Q → ¬ P→ ¬ P¬ P`

and pushes negations inside`P`

and`Q`

using`push_neg`

`contrapose h`

first reverts the local assumption`h`

, and then uses`contrapose`

and`intro h`

`contrapose! h`

first reverts the local assumption`h`

, and then uses`contrapose!`

and`intro h`

`contrapose h with new_h`

uses the name`new_h`

for the introduced hypothesis

Transforms the goal into its contrapositive.

`contrapose`

turns a goal`P → Q→ Q`

into`¬ Q → ¬ P¬ Q → ¬ P→ ¬ P¬ P`

`contrapose h`

first reverts the local assumption`h`

, and then uses`contrapose`

and`intro h`

`contrapose h with new_h`

uses the name`new_h`

for the introduced hypothesis

## Equations

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

Transforms the goal into its contrapositive and uses pushes negations inside `P`

and `Q`

.
Usage matches `contrapose`

## Equations

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