### Question

What is the difference between a lemma and a ghost method?

A lemma is a ghost method that does not have a modifies clause. Lemmas also do not typically return results. However, in most places where a lemma is used, it must be declared as a lemma. For example the lemma call that can be part of an expression must call a method that is declared to be a lemma, not a ghost method.