From Stdlib Require Import Utf8.
From Stdlib Require Import ZArith.

Require Import Core.

Notation "x ≤ y" := (x ≤ y)%Z (at level 70, y at next level) : Z_scope.
Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Z (at level 70, y at next level) :
  Z_scope.

Instance Z_ring_like_op : ring_like_op Z :=
  {| rngl_zero := 0%Z;
     rngl_one := 1%Z;
     rngl_add := Z.add;
     rngl_mul := Z.mul;
     rngl_opt_opp_or_psub := Some (inl Z.opp);
     rngl_opt_inv_or_pdiv := Some (inr Z.quot);
     rngl_opt_is_zero_divisor := None;
     rngl_opt_eq_dec := Some Z.eq_dec;
     rngl_opt_leb := Some Z.leb |}.

Theorem Z_eq_mul_0 : ∀ n m, (n × m)%Z = 0%Z → n = 0%Z ∨ m = 0%Z.

Theorem Z_integral :
  ∀ a b : Z,
  (a × b)%L = 0%L
  → a = 0%L ∨ b = 0%L ∨ rngl_is_zero_divisor a ∨ rngl_is_zero_divisor b.

Theorem Z_characteristic_prop : ∀ i, rngl_mul_nat 1 (S i) ≠ 0%Z.

Theorem Z_mul_le_compat_nonneg :
  ∀ a b c d : Z,
  (0 <=? a)%Z = true ∧ (a <=? c)%Z = true
  → (0 <=? b)%Z = true ∧ (b <=? d)%Z = true
  → (a × b <=? c × d)%Z = true.

Theorem Z_mul_le_compat_nonpos :
  ∀ a b c d : Z,
  (c <=? a)%Z = true ∧ (a <=? 0)%Z = true
  → (d <=? b)%Z = true ∧ (b <=? 0)%Z = true
  → (a × b <=? c × d)%Z = true.

Theorem Z_not_le :
  ∀ a b : Z, (a <=? b)%Z ≠ true → a ≠ b ∧ (b <=? a)%Z = true.

Theorem Z_opt_le_dec : ∀ a b : Z, {(a <=? b)%Z = true} + {(a <=? b)%Z ≠ true}.
Theorem Z_le_refl : ∀ a : Z, (a <=? a)%Z = true.

Theorem Z_le_antisymm :
  ∀ a b : Z, (a <=? b)%Z = true → (b <=? a)%Z = true → a = b.

Theorem Z_le_trans :
  ∀ a b c : Z, (a <=? b)%Z = true → (b <=? c)%Z = true → (a <=? c)%Z = true.

Theorem Z_add_le_mono_l :
  ∀ a b c, (b <=? c)%Z = true ↔ (a + b <=? a + c)%Z = true.
Theorem nat_archimedean : ∀ a b, (0 < a → ∃ₜ n, (n × a > b)%nat).

Theorem Pos2Nat_neq_0 : ∀ a, Pos.to_nat a ≠ 0%nat.

Theorem Pos_archimedean : ∀ a b, ∃ₜ n, (Pos.of_nat n × a > b)%positive.

Theorem Z_archimedean' : ∀ a b, (0 < a → ∃ₜ n, Z.of_nat n × a > b)%Z.


Theorem rngl_mul_nat_Z : ∀ z n, rngl_mul_nat z n = (Z.of_nat n × z)%Z.

Theorem Z_archimedean :
  ∀ a b : Z, (0 < a)%L → ∃ₜ n : nat, (b < rngl_mul_nat a n)%L.

Definition Z_ring_like_ord :=
  {| rngl_ord_le_dec := Z_opt_le_dec;
     rngl_ord_le_refl := Z_le_refl;
     rngl_ord_le_antisymm := Z_le_antisymm;
     rngl_ord_le_trans := Z_le_trans;
     rngl_ord_add_le_mono_l := Z_add_le_mono_l;
     rngl_ord_mul_le_compat_nonneg := Z_mul_le_compat_nonneg;
     rngl_ord_mul_le_compat_nonpos := Z_mul_le_compat_nonpos;
     rngl_ord_not_le := Z_not_le |}.

Definition Z_ring_like_prop : ring_like_prop Z :=
  {| rngl_mul_is_comm := true;
     rngl_is_archimedean := true;
     rngl_is_alg_closed := false;
     rngl_characteristic := 0;
     rngl_add_comm := Z.add_comm;
     rngl_add_assoc := Z.add_assoc;
     rngl_add_0_l := Z.add_0_l;
     rngl_mul_assoc := Z.mul_assoc;
     rngl_mul_1_l := Z.mul_1_l;
     rngl_mul_add_distr_l := Z.mul_add_distr_l;
     rngl_opt_mul_comm := Z.mul_comm;
     rngl_opt_mul_1_r := NA;
     rngl_opt_mul_add_distr_r := NA;
     rngl_opt_add_opp_diag_l := Z.add_opp_diag_l;
     rngl_opt_add_sub := NA;
     rngl_opt_sub_add_distr := NA;
     rngl_opt_sub_0_l := NA;
     rngl_opt_mul_inv_diag_l := NA;
     rngl_opt_mul_inv_diag_r := NA;
     rngl_opt_mul_div := Z.quot_mul;
     rngl_opt_integral := Z_integral;
     rngl_opt_alg_closed := NA;
     rngl_opt_characteristic_prop := Z_characteristic_prop;
     rngl_opt_ord := Z_ring_like_ord;
     rngl_opt_archimedean := Z_archimedean |}.