Round trip, case by case: indices, fractions, powers, cases

Lean module Esm.Document.Math.Cases7, formal/Esm/Document/Math/Cases7.lean at 184aa13d35e5
Imports Esm.Document.Math.Cases6

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