Library Presburger.PresTac_ex

Require Import PresTac.

Examples of application of the tactic

Theorem OddEven :
∀ x : BinInt.Z,
(∃ y : BinInt.Z , x = (y + y)%Z) ∨
(∃ y : BinInt.Z , x = (y + y + 1)%Z).
prestac.
Qed.

Theorem NOddEven :
∀ x : BinInt.Z,
¬
((∃ y : BinInt.Z , x = (y + y)%Z) ∧
(∃ y : BinInt.Z , x = (y + y + 1)%Z)).
prestac.
Qed.