Base case and inductive step as a solver sees them, why a true property may not be inductive, and how to strengthen an invariant until it closes.
Part of Discrete Mathematics for Formal Verification on formal.org.