Round trip, case by case: calls, min/max, initial conditions, indices

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

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