From Stdlib Require Import Utf8 Arith.

Require Import Core.

Instance nat_ring_like_op : ring_like_op nat :=
  {| rngl_zero := 0;
     rngl_one := 1;
     rngl_add := Nat.add;
     rngl_mul := Nat.mul;
     rngl_opt_opp_or_psub := Some (inr Nat.sub);
     rngl_opt_inv_or_pdiv := Some (inr Nat.div);
     rngl_opt_is_zero_divisor := None;
     rngl_opt_eq_dec := Some Nat.eq_dec;
     rngl_opt_leb := Some Nat.leb |}.


Theorem Nat_eq_mul_0 : ∀ n m, n × m = 0 → n = 0 ∨ m = 0.

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

Theorem nat_opt_characteristic_prop :
  let ro := nat_ring_like_op in
  ∀ i, rngl_mul_nat 1 (S i) ≠ 0.

Theorem Nat_mul_div :
  let ro := nat_ring_like_op in
  ∀ a b, b ≠ 0%L → (a × b / b)%L = a.

Theorem Nat_not_le :
  ∀ a b : nat, (a <=? b) ≠ true → a ≠ b ∧ (b <=? a) = true.

Theorem Nat_opt_le_dec :
  ∀ a b : nat, {(a <=? b) = true} + {(a <=? b) ≠ true}.

Theorem Nat_le_antisymm :
  ∀ a b : nat, (a <=? b) = true → (b <=? a) = true → a = b.

Theorem Nat_le_trans :
  ∀ a b c : nat, (a <=? b) = true → (b <=? c) = true → (a <=? c) = true.

Theorem Nat_add_le_mono_l :
  ∀ a b c, (b <=? c) = true ↔ (a + b <=? a + c) = true.
Theorem nat_rngl_mul_nat :
  let ro := nat_ring_like_op in
  ∀ a b, rngl_mul_nat a b = a × b.

Theorem nat_archimedean :
  let ro := nat_ring_like_op in
  ∀ a b : nat, (0 < a)%L → ∃ₜ n : nat, (b < rngl_mul_nat a n)%L.

Theorem Nat_mul_le_compat_nonneg :
  ∀ a b c d : nat, (0 ≤ a ≤ c)%L → (0 ≤ b ≤ d)%L → (a × b ≤ c × d)%L.

Theorem Nat_mul_le_compat_nonpos :
  ∀ a b c d : nat, (c ≤ a ≤ 0)%L → (d ≤ b ≤ 0)%L → (a × b ≤ c × d)%L.

Definition nat_ring_like_ord :=
  {| rngl_ord_le_dec := Nat_opt_le_dec;
     rngl_ord_le_refl := Nat.leb_refl;
     rngl_ord_le_antisymm := Nat_le_antisymm;
     rngl_ord_le_trans := Nat_le_trans;
     rngl_ord_add_le_mono_l := Nat_add_le_mono_l;
     rngl_ord_mul_le_compat_nonneg := Nat_mul_le_compat_nonneg;
     rngl_ord_mul_le_compat_nonpos := Nat_mul_le_compat_nonpos;
     rngl_ord_not_le := Nat_not_le |}.

Canonical Structure nat_ring_like_prop : ring_like_prop nat :=
  {| rngl_mul_is_comm := true;
     rngl_is_archimedean := true;
     rngl_is_alg_closed := false;
     rngl_characteristic := 0;
     rngl_add_comm := Nat.add_comm;
     rngl_add_assoc := Nat.add_assoc;
     rngl_add_0_l := Nat.add_0_l;
     rngl_mul_assoc := Nat.mul_assoc;
     rngl_mul_1_l := Nat.mul_1_l;
     rngl_mul_add_distr_l := Nat.mul_add_distr_l;
     rngl_opt_mul_comm := Nat.mul_comm;
     rngl_opt_mul_1_r := NA;
     rngl_opt_mul_add_distr_r := NA;
     rngl_opt_add_opp_diag_l := NA;
     rngl_opt_add_sub := Nat.add_sub;
     rngl_opt_sub_add_distr := Nat.sub_add_distr;
     rngl_opt_sub_0_l := Nat.sub_0_l;
     rngl_opt_mul_inv_diag_l := NA;
     rngl_opt_mul_inv_diag_r := NA;
     rngl_opt_mul_div := Nat_mul_div;
     rngl_opt_integral := Nat_eq_mul_0';
     rngl_opt_alg_closed := NA;
     rngl_opt_characteristic_prop := nat_opt_characteristic_prop;
     rngl_opt_ord := nat_ring_like_ord;
     rngl_opt_archimedean := nat_archimedean |}.




Instance lcm_ring_like_op : ring_like_op nat :=
  {| rngl_zero := 1;
     rngl_one := 1;
     rngl_add := Nat.lcm;
     rngl_mul := Nat.mul;
     rngl_opt_opp_or_psub := None;
     rngl_opt_inv_or_pdiv := None;
     rngl_opt_is_zero_divisor := None;
     rngl_opt_eq_dec := Some Nat.eq_dec;
     rngl_opt_leb := None |}.

Section a.

Context (ro := lcm_ring_like_op).

Theorem lcm_mul_add_distr_l : ∀ a b c,
  a × Nat.lcm b c = Nat.lcm (a × b) (a × c).

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

Theorem lcm_characteristic_prop :
  let rol := lcm_ring_like_op in
  if 1 =? 0 then ∀ i : nat, rngl_mul_nat 1 (S i) ≠ 0%L
  else (∀ i, 0 < i < 1 → rngl_mul_nat 1 i ≠ 0%L) ∧ rngl_mul_nat 1 1 = 0%L.

Definition lcm_ring_like_prop :=
  let rol := lcm_ring_like_op in
  {| rngl_mul_is_comm := true;
     rngl_is_archimedean := false;
     rngl_is_alg_closed := false;
     rngl_characteristic := 1;
     rngl_add_comm := Nat.lcm_comm;
     rngl_add_assoc := Nat.lcm_assoc;
     rngl_add_0_l := Nat.lcm_1_l;
     rngl_mul_assoc := Nat.mul_assoc;
     rngl_mul_1_l := Nat.mul_1_l;
     rngl_mul_add_distr_l := lcm_mul_add_distr_l;
     rngl_opt_mul_comm := Nat.mul_comm;
     rngl_opt_mul_1_r := NA;
     rngl_opt_mul_add_distr_r := NA;
     rngl_opt_add_opp_diag_l := NA;
     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 := NA;
     rngl_opt_integral := lcm_opt_integral;
     rngl_opt_alg_closed := NA;
     rngl_opt_characteristic_prop := lcm_characteristic_prop;
     rngl_opt_ord := NA;
     rngl_opt_archimedean := NA |}.

End a.