(* Some small examples, because the method is exponential *)

Lemma exemple1 : forall a b, negb (orb a b) = andb (negb a) (negb b).
intros. validity.
Qed.

Lemma exemple2 : forall a b c,
negb a || negb b || (c && true) = negb (a && b && negb c).
intros. validity.
Qed.

Lemma exemple3 : forall a,
negb (negb a) = a.
intros. validity.
Qed.

Lemma exemple4 : forall a b, a && a && b = b && b && a.
intros. validity.
Qed.

Lemma exemple5 : forall a b c,
(a && b) || (negb a && c) = (negb a || b) && (a || c).
intros. validity.
Qed.

(* This example fails because the identity is false *)
Lemma false_ex1 : forall a b,
a || b = negb a || negb b.
intros. validity. admit.
Qed.

(* This example fails because of the method can't see that
   n1 >= n2 and n2 >= n1 are related *)
Lemma false_ex2 : forall n1 n2 : nat,
greater_eq n1 n2 || greater_eq n2 n1 = true.
intros. validity. admit.
Qed.