Require Import RingLike.Core.

From Stdlib Require Import Utf8 Arith.
Require Import Structures.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.

Theorem rngl_add_0_r : ∀ a, (a + 0 = a)%L.

Theorem rngl_add_opp_l :
  rngl_has_opp T = true →
  ∀ a b, (- a + b)%L = (b - a)%L.

Theorem rngl_add_opp_r :
  rngl_has_opp T = true →
  ∀ a b, (a + - b)%L = (a - b)%L.

Theorem rngl_add_opp_diag_l :
  rngl_has_opp T = true →
  ∀ x, (- x + x = 0)%L.

Theorem rngl_sub_diag :
  rngl_has_opp_or_psub T = true →
  ∀ a, (a - a = 0)%L.

Theorem rngl_psub_diag :
  rngl_has_opp_or_psub T = true →
  ∀ a, rngl_psub a a = 0%L.

Theorem rngl_sub_add :
  rngl_has_opp T = true →
  ∀ a b, (a - b + b = a)%L.

Theorem rngl_add_sub :
  rngl_has_opp_or_psub T = true →
  ∀ a b, (a + b - b = a)%L.

Theorem rngl_add_cancel_l :
  rngl_has_opp_or_psub T = true →
  ∀ a b c, (a + b = a + c)%L ↔ (b = c)%L.

Theorem rngl_add_cancel_r :
  rngl_has_opp_or_psub T = true →
  ∀ a b c, (a + c = b + c)%L ↔ (a = b)%L.

Theorem rngl_add_move_l :
  rngl_has_opp T = true →
  ∀ a b c, (a + b)%L = c ↔ b = (c - a)%L.
Theorem rngl_add_move_r :
  rngl_has_opp T = true →
  ∀ a b c, (a + b)%L = c ↔ a = (c - b)%L.

Theorem rngl_sub_move_l :
  rngl_has_opp T = true →
  ∀ a b c, (a - b)%L = c ↔ b = (a - c)%L.
Theorem rngl_sub_move_r :
  rngl_has_opp T = true →
  ∀ a b c, (a - b)%L = c ↔ a = (c + b)%L.
Theorem rngl_add_sub_eq_l :
  rngl_has_opp_or_psub T = true →
  ∀ a b c, (a + b = c → c - a = b)%L.

Theorem rngl_add_sub_eq_r :
  rngl_has_opp_or_psub T = true →
   ∀ a b c, (a + b = c → c - b = a)%L.

Theorem rngl_sub_compat_l : ∀ a b c,
  a = b → (a - c = b - c)%L.

Theorem rngl_add_move_0_l :
  rngl_has_opp T = true →
  ∀ a b, (a + b = 0)%L ↔ (b = - a)%L.
Theorem rngl_add_move_0_r :
  rngl_has_opp T = true →
  ∀ a b, (a + b = 0)%L ↔ (a = - b)%L.

Theorem rngl_add_compat_r : ∀ a b c,
  (a = b)%L → (a + c = b + c)%L.

Theorem rngl_sub_move_0_r :
  rngl_has_opp T = true →
  ∀ a b : T, (a - b)%L = 0%L ↔ a = b.
Theorem rngl_opp_0 : rngl_has_opp T = true → (- 0 = 0)%L.

Theorem rngl_psub_0_r :
  rngl_has_psub T = true →
  ∀ a, rngl_psub a 0%L = a.

Theorem rngl_sub_0_l :
  rngl_has_opp T = true →
  ∀ a, (0 - a = - a)%L.

Theorem rngl_sub_0_r :
  rngl_has_opp_or_psub T = true →
  ∀ a, (a - 0 = a)%L.

Theorem rngl_opp_add_distr :
  rngl_has_opp T = true →
  ∀ a b, (- (a + b) = - a - b)%L.

Theorem rngl_opp_sub_swap :
  rngl_has_opp T = true →
  ∀ a b, (- a - b = - b - a)%L.

Theorem rngl_add_add_swap : ∀ a b c, (a + b + c = a + c + b)%L.

Theorem rngl_add_add_add_swap :
  ∀ a b c d, ((a + b) + (c + d) = (a + c) + (b + d))%L.

Theorem rngl_sub_sub_swap :
  rngl_has_opp T = true →
  ∀ a b c, (a - b - c = a - c - b)%L.

Theorem rngl_add_compat_l : ∀ a b c,
  (a = b)%L → (c + a = c + b)%L.

Theorem rngl_add_sub_assoc :
  rngl_has_opp T = true →
  ∀ a b c, (a + (b - c) = a + b - c)%L.

Theorem rngl_add_sub_swap :
  rngl_has_opp T = true →
  ∀ a b c, (a + b - c = a - c + b)%L.

Theorem rngl_add_sub_simpl_l :
  rngl_has_opp_or_psub T = true →
  ∀ a b c : T, (a + b - (a + c) = b - c)%L.

Theorem rngl_opp_involutive :
  rngl_has_opp T = true →
  ∀ x, (- - x)%L = x.

Theorem rngl_sub_opp_r :
  rngl_has_opp T = true →
  ∀ a b, (a - - b = a + b)%L.

Theorem rngl_opp_inj :
  rngl_has_opp T = true →
  ∀ a b, (- a = - b)%L → a = b.

Theorem rngl_sub_cancel_l :
  rngl_has_opp T = true →
  ∀ a b c, (a - b)%L = (a - c)%L ↔ b = c.

Theorem rngl_opp_sub_distr :
  rngl_has_opp T = true →
  ∀ a b, (- (a - b) = b - a)%L.

Theorem rngl_sub_add_distr :
  rngl_has_opp_or_psub T = true →
  ∀ a b c, (a - (b + c) = a - b - c)%L.

Theorem rngl_sub_sub_distr :
  rngl_has_opp T = true →
  ∀ a b c, (a - (b - c) = a - b + c)%L.

Theorem rngl_mul_nat_add_r : ∀ a m n,
  rngl_mul_nat a (m + n) = (rngl_mul_nat a m + rngl_mul_nat a n)%L.

Theorem rngl_of_nat_add : ∀ m n,
  rngl_of_nat (m + n) = (rngl_of_nat m + rngl_of_nat n)%L.

Theorem rngl_of_nat_sub :
  rngl_has_opp_or_psub T = true →
  ∀ m n, n ≤ m → rngl_of_nat (m - n) = (rngl_of_nat m - rngl_of_nat n)%L.

Theorem rngl_of_nat_1 : rngl_of_nat 1 = 1%L.

Theorem rngl_of_nat_2 : rngl_of_nat 2 = 2%L.

Theorem rngl_of_nat_3 : rngl_of_nat 3 = 3%L.

Theorem rngl_mul_nat_succ :
  ∀ a n, rngl_mul_nat a (S n) = (a + rngl_mul_nat a n)%L.

Theorem rngl_of_nat_succ :
  ∀ n, rngl_of_nat (S n) = (1 + rngl_of_nat n)%L.

Theorem rngl_abs_0 :
  rngl_has_opp T = true →
  ∣ 0 ∣ = 0%L.

Theorem eq_rngl_abs_0 :
  rngl_has_opp T = true →
  ∀ a, rngl_abs a = 0%L → a = 0%L.

Theorem rngl_add_opp_diag_r :
  rngl_has_opp T = true →
  ∀ x : T, (x + - x)%L = 0%L.

Arguments rngl_mul_nat {T ro} a%_L n%_nat.

Theorem rngl_of_nat_0 : rngl_of_nat 0 = 0%L.

Theorem fold_rngl_mul_nat :
  ∀ a n, List.fold_right rngl_add 0%L (List.repeat a n)%L = rngl_mul_nat a n.

Theorem rngl_characteristic_0 :
  rngl_characteristic T = 0 →
  ∀ i : nat, rngl_of_nat (S i) ≠ 0%L.

Theorem rngl_characteristic_non_0 :
  rngl_characteristic T ≠ 0 →
  (∀ i : nat, 0 < i < rngl_characteristic T → rngl_of_nat i ≠ 0%L) ∧
  rngl_of_nat (rngl_characteristic T) = 0%L.

Theorem rngl_1_neq_0 : rngl_characteristic T ≠ 1 → (1 ≠ 0)%L.

Theorem rngl_1_neq_0_iff : rngl_characteristic T ≠ 1 ↔ (1 ≠ 0)%L.

Theorem eq_rngl_of_nat_0 :
  rngl_characteristic T = 0 →
  ∀ i, rngl_of_nat i = 0%L → i = 0.

End a.

Arguments rngl_abs {T ro} a%_L.
Arguments rngl_add_sub {T ro rp} Hom (a b)%_L.
Arguments rngl_add_sub_assoc {T ro rp} Hop (a b c)%_L.
Arguments rngl_add_add_swap {T ro rp} (a b c)%_L.
Arguments rngl_add_sub_swap {T ro rp} Hop (a b c)%_L.
Arguments rngl_min {T ro} (a b)%_L.
Arguments rngl_mul_nat {T ro} a%_L n%_nat.
Arguments rngl_opp_sub_swap {T ro rp} Hop (a b)%_L.
Arguments rngl_sub_add {T ro rp} Hop (a b)%_L.
Arguments rngl_sub_add_distr {T ro rp} Hos (a b c)%_L.
Arguments rngl_sub_sub_swap {T ro rp} Hop (a b c)%_L.