HOL-ex.Triangular_Numbers