// Assume unknown predicates for evenness and oddness.

ghost predicate Even(n: nat)
ghost predicate Odd(n: nat)

// Assume lemmas to explain what the predicates mean.

lemma EvenP()
  ensures forall n: nat :: Even(n) == exists m: nat :: n == 2 * m
lemma OddP()
  ensures forall n: nat :: Odd(n) == !Even(n)

// Here is a proof:

lemma SuccOddIsEven()
  ensures forall n: nat :: Odd(n) ==> Even(n + 1)
{
  EvenP();
  OddP();

  assert forall a: nat :: a % 2 == 0 ==> a == 2 * (a / 2);
  assert forall b: nat :: b == 2 * (b / 2) ==> Even(b);
  assert forall c: nat :: Odd(c) ==> c % 2 == 1;
  assert forall d: nat :: d % 2 == 1 ==> (d + 1) % 2 == 0;
}

// Reorganize it by making the arbitrary `n` a parameter with a requirement,
// and by moving the general statement about `Even` to its own lemma:

lemma SuccOddIsEven'()
  requires false
  ensures Even(n + 1)
{
  EvenP();
  OddP();
  SomethingSomethingAboutEven();

  assert forall a: nat :: a % 2 == 0 ==> a == 2 * (a / 2);
  assert forall b: nat :: b == 2 * (b / 2) ==> Even(b);
  assert forall c: nat :: Odd(c) ==> c % 2 == 1;
  assert forall d: nat :: d % 2 == 1 ==> (d + 1) % 2 == 0;
}

lemma SomethingSomethingAboutEven()
  ensures false
{
}