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?