Negation introduction. The negation ¬A is derived by leading the assumption A to a contradiction. It must be distinguished from the classical reductio ad absurdum, (H ∧ ¬A ⊢ ⊥) → (H ⊢ A), which adds the subsequent application of dne to neg_intro and is therefore not part of intuitionistic logic.