Library HoTT.Classes.orders.naturals

Require Import
  HoTT.Types.Sigma.
Require Import
  HoTT.Classes.theory.naturals.
Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.rings
  HoTT.Classes.orders.rings
  HoTT.Classes.implementations.peano_naturals.
Require Export
  HoTT.Classes.orders.nat_int.

Generalizable Variables N R Rle Rlt f.

Section naturals_order.
Context `{Funext} `{Univalence}.
Context `{Naturals N} `{!TrivialApart N}.

Instance nat_nonneg x : PropHolds (0 ≤ x).
Proof. apply (to_semiring_nonneg (f:=id)). Qed.

Lemma nat_le_plus {x y: N}: x ≤ y ↔ ∃ z, y = x + z.
Proof.
split; intros E.
- destruct (decompose_le E) as [z [Ez1 Ez2]]. ∃ z. trivial.
- destruct E as [z Ez].
  apply compose_le with z; [solve_propholds | trivial].
Qed.

Lemma nat_not_neg x : ~(x < 0).
Proof. apply le_not_lt_flip, nat_nonneg. Qed.

Lemma nat_0_or_pos x : x = 0 |_| 0 < x.
Proof.
destruct (trichotomy (<) 0 x) as [?|[?|?]]; auto.
- left;symmetry;trivial.
- destruct (nat_not_neg x). trivial.
Qed.

Lemma nat_0_or_ge_1 x : x = 0 |_| 1 ≤ x.
Proof.
destruct (nat_0_or_pos x);auto.
right;apply pos_ge_1. trivial.
Qed.

Lemma nat_ne_0_pos x : x ≠ 0 ↔ 0 < x.
Proof.
split.
- destruct (nat_0_or_pos x); auto.
  intros E;destruct E;trivial.
- intros E1 E2. rewrite E2 in E1. destruct (irreflexivity (<) 0). trivial.
Qed.

Lemma nat_ne_0_ge_1 x : x ≠ 0 ↔ 1 ≤ x.
Proof.
etransitivity.
- apply nat_ne_0_pos.
- apply pos_ge_1.
Qed.

Global Instance: ∀ (z : N), PropHolds (z ≠ 0) → OrderReflecting (z *.).
Proof.
intros z ?. red. apply (order_reflecting_pos (.*.) z).
apply nat_ne_0_pos. trivial.
Qed.

Global Instance slow_nat_le_dec: ∀ x y: N, Decidable (x ≤ y) | 10.
Proof.
intros x y.
destruct (nat_le_dec (naturals_to_semiring _ nat x) (naturals_to_semiring _ nat y))
as [E | E].
- left.
  apply (order_reflecting (naturals_to_semiring N nat)). exact E.
- right. intros E'. apply E.
  apply order_preserving;trivial. apply _.
Qed.

Section another_ring.
  Context `{IsCRing R} `{Apart R} `{!FullPseudoSemiRingOrder (A:=R) Rle Rlt}
    `{!IsSemiRingPreserving (f : N → R)}.

  Lemma negate_to_ring_nonpos n : -f n ≤ 0.
  Proof. apply flip_nonneg_negate. apply to_semiring_nonneg. Qed.

  Lemma between_to_ring n : -f n ≤ f n.
  Proof. apply between_nonneg. apply to_semiring_nonneg. Qed.
End another_ring.
End naturals_order.

#[export]
Hint Extern 20 (PropHolds (_ ≤ _)) ⇒ eapply @nat_nonneg : typeclass_instances.