possible minor error in the fp in lean book?

Stream: lean4

[Calvin]

Hiya :wave: I've been following along with the FP in Lean book (which has been absolutely great so far) and I think one of the exercises has a copy-paste error? Specifically, in the interlude about proofs it asks to prove 5 < 18 using rfl, which I don't think makes sense? For context, it's one among other propositions (that all do use =) in that example and the very next example asks to prove the same props using by simp which would make sense for 5 < 18, and is why I think this is just a small editing error. Just looking for clarification in my understanding or to report this error :smile:

[Wojciech Nawrocki]

That does sound like an error! There is a thread about the book you could report this on.