# Reverse contraposition

While it is trivial to prove contraposition

∀ A B: Prop, (A → B) → (~B → ~A)


using Coq, is it equally trivial to prove the reversed form:

∀ A B: Prop, (~A → ~B) → (B → A)


? In particular, is it doable without using any additional axioms, e.g. from classical logic?

It is not provable without additional axioms. In fact, it implies double negation elimination (take $B=\top$), which in turn is equivalent to the excluded middle.