Theorem abs_sub_nonpos

Modification history

2024-02-23 19:51

Mathlib/Algebra/Order/Group/Abs.lean

feat: Small lemmas around |a - b| and Int.natAbs (a - b) (#10027) …

Added abs_sub_nonpos View on Github →