orders.integers

Require
  theory.integers theory.int_abs.
Require Import
  Ring workaround_tactics
  abstract_algebra interfaces.integers interfaces.naturals interfaces.additional_operations interfaces.orders
  natpair_integers orders.rings orders.naturals theory.rings.

Section integers_order.
Context `{Integers Int} `{Apart Int} `{!TrivialApart Int} `{!FullPseudoSemiRingOrder Intle Intlt}.

Lemma integers_le_plus (x y: Int) : x y z: nat, y = x + naturals_to_semiring nat Int z.

Section another_ring.
  Context `{Ring R} `{Apart R} `{!FullPseudoSemiRingOrder (A:=R) Rle Rlt} {f : Int R} `{!SemiRing_Morphism f}.

  Let f_preserves_nonneg x : 0 x 0 f x.

  Global Instance morphism_order_preserving: OrderPreserving f.

  Context `{!Injective f}.
  Let f_preserves_nonneg_back x : 0 f x 0 x.

  Global Instance: OrderEmbedding f.
End another_ring.
End integers_order.

Section other_results.
Context `{Integers Int} `{Apart Int} `{!TrivialApart Int} `{!FullPseudoSemiRingOrder Intle Intlt}.
Add Ring Int : (rings.stdlib_ring_theory Int).

Global Program Instance: x y: Int, Decision (x y) | 10 := λ x y,
  match decide (integers_to_ring _ (SRpair nat) x integers_to_ring _ (SRpair nat) y) with
  | left E => left _
  | right E => right _
  end.

Add Ring nat : (stdlib_semiring_theory nat).

Lemma le_iff_lt_plus_1 x y : x y x < y + 1.

Lemma lt_iff_plus_1_le x y : x < y x + 1 y.

Lemma induction
  (P: Int Prop) `{!Proper ((=) ==> iff) P}:
  P 0 ( n, 0 n P n P (1 + n)) ( n, n 0 P n P (n - 1)) n, P n.

Lemma induction_nonneg
  (P: Int Prop) `{!Proper ((=) ==> iff) P}:
  P 0 ( n, 0 n P n P (1 + n)) n, 0 n P n.

Global Instance biinduction: Biinduction Int.
End other_results.

Instance int_le `{Integers Z} : Le Z | 10 := λ x y, z, y = x + naturals_to_semiring nat Z z.
Instance int_lt `{Integers Z} : Lt Z | 10 := dec_lt.

Section default_order.
Context `{Integers Int} `{Apart Int} `{!TrivialApart Int}.
Add Ring Int2 : (rings.stdlib_ring_theory Int).

Instance: Proper ((=) ==> (=) ==> iff) int_le.

Instance: PartialOrder int_le.

Instance: SemiRingOrder int_le.

Notation i_to_r := (integers_to_ring Int (SRpair nat)).

Instance: TotalRelation int_le.

Global Instance: FullPseudoSemiRingOrder int_le int_lt.
End default_order.