theory.int_abs

Require
  theory.nat_distance.
Require Import
  interfaces.naturals abstract_algebra interfaces.orders natpair_integers
  theory.integers theory.rings orders.naturals orders.rings.

Section contents.
Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt} `{Naturals N}.

Lemma int_abs_uniq (a b : IntAbs Z N) (z : Z) : a z = b z.

Global Program Instance slow_int_abs: IntAbs Z N | 10 :=
  λ x, (int_abs (SRpair N) N (integers_to_ring Z (SRpair N) x))↾_.

Context `{!IntAbs Z N}.

Global Instance int_abs_proper: Proper ((=) ==> (=)) (int_abs Z N).

Lemma int_abs_nat (n: N) : int_abs Z N (naturals_to_semiring N Z n) = n.

Lemma int_abs_opp_nat (n: N) : int_abs Z N (-naturals_to_semiring N Z n) = n.

Lemma int_abs_neg_is_pos (x y: N) :
  - naturals_to_semiring N Z x = naturals_to_semiring N Z y x = 0 y = 0.

Lemma int_abs_nonneg x : 0 x naturals_to_semiring N Z (int_abs Z N x) = x.

Lemma int_abs_nonneg_plus x y :
  0 x 0 y int_abs Z N (x + y) = int_abs Z N x + int_abs Z N y.

Lemma int_abs_0 : int_abs Z N 0 = 0.

Lemma int_abs_0_alt x : int_abs Z N x = 0 x = 0.

Lemma int_abs_ne_0 x : int_abs Z N x 0 x 0.

Lemma int_abs_nonneg_mult x y :
  0 x 0 y int_abs Z N (x * y) = int_abs Z N x * int_abs Z N y.

Lemma int_abs_1 : int_abs Z N 1 = 1.

Lemma int_abs_opp z : int_abs Z N (- z) = int_abs Z N z.
End contents.