norm_num plugin for abs

TODO: plugins for mabs, norm, nnorm, and enorm.

theorem Mathlib.Meta.NormNum.isNat_abs_nonneg {α : Type u_1} [Ring α] [Lattice α] [IsOrderedRing α] {a : α} {na : ℕ} (pa : IsNat a na) : IsNat |a| na

theorem Mathlib.Meta.NormNum.isNat_abs_neg {α : Type u_1} [Ring α] [Lattice α] [IsOrderedRing α] {a : α} {na : ℕ} (pa : IsInt a (Int.negOfNat na)) : IsNat |a| na

theorem Mathlib.Meta.NormNum.isNNRat_abs_nonneg {α : Type u_1} [DivisionRing α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {num den : ℕ} (ra : IsNNRat a num den) : IsNNRat |a| num den

theorem Mathlib.Meta.NormNum.isNNRat_abs_neg {α : Type u_1} [DivisionRing α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {num den : ℕ} (ra : IsRat a (Int.negOfNat num) den) : IsNNRat |a| num den

def Mathlib.Meta.NormNum.evalAbs : NormNumExt

The norm_num extension which identifies expressions of the form |a|, such that norm_num successfully recognises a.