orders.naturals

Require
  theory.naturals.
Require Import
  Morphisms Ring Program
  abstract_algebra interfaces.naturals interfaces.orders
  orders.rings theory.rings.

Section naturals_order.
Context `{Naturals N} `{Apart N} `{!TrivialApart N} `{!FullPseudoSemiRingOrder Nle Nlt}.

Lemma to_semiring_nonneg `{SemiRing R} `{Apart R} `{!FullPseudoSemiRingOrder (A:=R) Rle Rlt}
  `{!SemiRing_Morphism (f : N R)} n : 0 f n.

Lemma naturals_nonneg x : 0 x.

Lemma natural_le_plus {x y: N}: x y z: N, y = x + z.

Section another_semiring.
  Context `{SemiRing R} `{Apart R} `{!FullPseudoSemiRingOrder (A:=R) Rle Rlt}
    {f : N R} `{!SemiRing_Morphism f}.

  Global Instance morphism_order_preserving: OrderPreserving f.
End another_semiring.

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

  Lemma opp_to_semiring_nonpos n : - naturals_to_semiring N R n 0.

  Lemma opp_to_sr_le_to_sr n : - naturals_to_semiring N R n naturals_to_semiring N R n.

  Lemma opp_to_semiring x y : - naturals_to_semiring N R x = naturals_to_semiring N R y
     naturals_to_semiring N R x = naturals_to_semiring N R y.
End another_ring.
End naturals_order.

Section order_unique.
Context `{Naturals N} `{Naturals N2} {f : N N2} `{!SemiRing_Morphism f}
  `{Apart N} `{!TrivialApart N} `{!FullPseudoSemiRingOrder (A:=N) Nle Nlt}
  `{Apart N2} `{!TrivialApart N2} `{!FullPseudoSemiRingOrder (A:=N2) N2le N2lt}.

Global Instance: OrderEmbedding f.
End order_unique.

Section other_results.
Context `{Naturals N} `{Apart N} `{!TrivialApart N} `{!FullPseudoSemiRingOrder Nle Nlt}.
Add Ring N : (stdlib_semiring_theory N).

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

Lemma ne_0_ge_1 x : x 0 1 x.

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.

Global Instance: (z : N), PropHolds (z 0) OrderPreservingBack (z *.).
End other_results.

Instance nat_le `{Naturals N} : Le N | 10 := λ x y, z, x + z = y.
Instance nat_lt `{Naturals N} : Lt N | 10 := dec_lt.

Section default_order.
Context `{Naturals N} `{Apart N} `{!TrivialApart N}.
Add Ring N2 : (rings.stdlib_semiring_theory N).

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

Instance: SemiRingOrder nat_le.

Notation n_to_sr := (naturals_to_semiring N nat).

Instance: TotalRelation nat_le.

Global Instance: FullPseudoSemiRingOrder nat_le nat_lt.
End default_order.