orders.rationals

Require Import
  Ring Field
  abstract_algebra interfaces.orders
  interfaces.naturals interfaces.rationals interfaces.integers
  natpair_integers theory.rationals theory.dec_fields theory.rings
  orders.integers orders.dec_fields.

Section rationals_and_integers.
  Context `{Rationals Q} `{!SemiRingOrder Qle}
    Z `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder (A:=Z) Zle Zlt}
    {f : Z Q} `{!SemiRing_Morphism f}.
  Add Field Q : (stdlib_field_theory Q).

  Lemma rationals_decompose_pos_den x :
     num, den, 0 < den x = f num / f den.
End rationals_and_integers.

Section rationals_and_another_rationals.
  Context `{Rationals Q1} `{Apart Q1} `{!TrivialApart Q1} `{!FullPseudoSemiRingOrder (A:=Q1) Q1le Q1lt}.
  Context `{Rationals Q2} `{Apart Q2} `{!TrivialApart Q2} `{!FullPseudoSemiRingOrder (A:=Q2) Q2le Q2lt}
     {f : Q1 Q2} `{!SemiRing_Morphism f}.

  Add Field Q1 : (stdlib_field_theory Q1).

  Notation i_to_r := (integers.integers_to_ring (SRpair nat) Q1).

  Let f_preserves_nonneg x : 0 x 0 f x.

  Instance morphism_order_preserving: OrderPreserving f.
End rationals_and_another_rationals.

Section rationals_order_isomorphic.
  Context `{Rationals Q1} `{Apart Q1} `{!TrivialApart Q1} `{!FullPseudoSemiRingOrder (A:=Q1) Q1le Q1lt}
    `{Rationals Q2} `{Apart Q2} `{!TrivialApart Q2} `{!FullPseudoSemiRingOrder (A:=Q2) Q2le Q2lt}
     {f : Q1 Q2} `{!SemiRing_Morphism f}.

  Global Instance: OrderEmbedding f.
End rationals_order_isomorphic.

Instance rationals_le `{Rationals Q} : Le Q | 10 := λ x y,
     num, den, y = x + naturals_to_semiring nat Q num / naturals_to_semiring nat Q den.
Instance rationals_lt `{Rationals Q} : Lt Q | 10 := dec_lt.

Section default_order.
  Context `{Rationals Q} `{Apart Q} `{!TrivialApart Q}.

  Add Field F: (stdlib_field_theory Q).
  Notation n_to_sr := (naturals_to_semiring nat Q).

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

  Instance: Reflexive rationals_le.

  Lemma rationals_decompose_le (x y: Q) :
    x y num, den, den 0 y = x + n_to_sr num * / n_to_sr den.

  Instance: Transitive rationals_le.

  Instance: AntiSymmetric rationals_le.

  Instance: PartialOrder rationals_le.

  Instance: SemiRingOrder rationals_le.

  Notation i_to_r := (integers_to_ring (SRpair nat) Q).
  Instance: TotalRelation rationals_le.

  Global Instance: FullPseudoSemiRingOrder rationals_le rationals_lt.
End default_order.