mathlib

741d2851 - chore(number_theory/zsqrtd/basic): simplify le_total proof (#13555)