# On Negation

Prove the following propositions:
~ False
forall P:Prop, ~ ~ ~ P -> ~ P
forall P Q:Prop, ~ ~ ~ P -> P -> Q
forall P Q:Prop, (P -> Q) -> ~ Q -> ~ P.
forall P Q R:Prop, (P -> Q) -> (P -> ~ Q) -> P -> R.

Some of these propositions don't need `False`-elimination;
in these situations, show that these theorems are derived from some
theorems of the minimal propositional logic.
## Solution

See on_negation.v
## Notes

Whenever `False`-elimination is not
needed, we first proved some lemma in minimal propositional logic, then
apply it to derive the statement we wanted to prove.

Please notice that all these results could be proved in one step :
either by "`unfold not; auto`" if `False`-elimination is not needed,
or by `tauto` in the other case.

Going home

Pierre Castéran