Require Import Omega.
Require Import ThinkArith.

Section TEST.

Variable SIZE : nat.
Variable i : nat.

Lemma test : SIZE - pred i - S (pred i - pred i) = 0.
  try omega.
  try omega2.
Admitted. (** not meant to be true **)

End TEST.