Round trip, case by case: ifelse as cases

Lean module Esm.Document.Math.Cases9, formal/Esm/Document/Math/Cases9.lean at 184aa13d35e5
Imports Esm.Document.Math.Cases8

This module also proves 2 lemmas without doc comments; they are in the source.