Theorem Int.natAbs_coe_sub_coe_lt_of_lt

Modification history

2024-02-23 19:51
Mathlib/Data/Int/Lemmas.lean
feat: Small lemmas around |a - b| and Int.natAbs (a - b) (#10027) …
Added Int.natAbs_coe_sub_coe_lt_of_ltView on Github →