---
tags: []
---

# Negation Introduction

This is also known as _proof by contradiction_. You start with an assumption
declared in a sub-proof. If you can derive a contradiction from this assumption
(typically from the introduction of another proposition and its negation), then
you are permitted to derive the negation of the auxiliary assumption in the main
proof.

![](/img/negate-intro.png)
