factorial simp example

[PatrickMassot]

In Chapter 5, we have

example : fac 0 = 1 := by
  simp [fac]

which is misleading since giving [fac] plays no role.

[avigad]

@PatrickMassot Is this a problem? The example right before shows that this particular case is solved by rfl. But, more generally, simp [fac] will replace fac 0 by 1 in any context. It seems strange to modify the example just to make that point.

A bigger issue is that we now only have a minimal discussion of decide in 5.3, and we never say that simp calls decide. Shall we replace this issue by a separate issue that says that we should expand the discussion of decide?