Definition abs_eq
Definition.
abs_eq
abs x = if (0 ≤ x) x (-x)
The
absolute value
of a real number x, defined as
|x| :=
if
x ≥ 0 then x else -x.