Div_with_order

Theorems about inverse and division, in the case when order relation exists.

Division can be either:

multiplication by the inverse (ab⁻¹) or
partial division (with the property ab/b=a).

A ring-like has an order when the variable rngl_is_ordered is true.

See the module RingLike.Core for the general description of the ring-like library.

In general, it is not necessary to import the present module. The normal usage is to do:

    Require Import RingLike.Core.

which imports the present module and some other ones.

From Stdlib Require Import Utf8 Arith.

Require Import Structures.
Require Import Order.
Require Import Add.
Require Import Mul.
Require Import Div.
Require Import Add_with_order.
Require Import Mul_with_order.

Section a.

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

Theorem rngl_inv_pos :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 < a → 0 < a⁻¹)%L.

Theorem rngl_inv_neg :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a, (a < 0 → a⁻¹ < 0)%L.

Theorem rngl_div_le_1 :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (b ≠ 0 → 0 ≤ a ≤ b → a / b ≤ 1)%L.

Theorem rngl_one_sub_half :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  (1 - 2⁻¹ = 2⁻¹)%L.

Theorem rngl_integral :
  rngl_has_opp_or_psub T = true →
  (rngl_is_integral_domain T ||
   rngl_has_inv_or_pdiv T && rngl_has_eq_dec_or_order T)%bool = true →
  ∀ a b, (a × b = 0)%L → a = 0%L ∨ b = 0%L.
Theorem rngl_abs_div :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ x y, y ≠ 0%L → rngl_abs (x / y)%L = (rngl_abs x / rngl_abs y)%L.
Theorem rngl_mul_pos_pos :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < a)%L → (0 < b)%L → (0 < a × b)%L.

Theorem rngl_mul_pos_cancel_r :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < b → 0 < a × b ↔ 0 < a)%L.
Theorem rngl_mul_pos_cancel_l :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < a → 0 < a × b ↔ 0 < b)%L.
Theorem rngl_mul_le_mono_pos_l :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (0 < a)%L → (b ≤ c)%L ↔ (a × b ≤ a × c)%L.
Theorem rngl_mul_lt_mono_pos_l :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (0 < a)%L → (b < c)%L ↔ (a × b < a × c)%L.
Theorem rngl_mul_lt_mono_pos_r :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (0 < a)%L → (b < c)%L ↔ (b × a < c × a)%L.
Theorem rngl_mul_le_mono_pos_r :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (0 < c)%L → (a ≤ b)%L ↔ (a × c ≤ b × c)%L.
Theorem rngl_div_lt_mono_pos_r :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (0 < a)%L → (b < c)%L ↔ (b / a < c / a)%L.
Theorem rngl_div_le_mono_pos_l :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 < a)%L → (b⁻¹ ≤ c⁻¹ ↔ a / b ≤ a / c)%L.

Theorem rngl_div_le_mono_pos_r :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 < c)%L → (a ≤ b ↔ a / c ≤ b / c)%L.

Theorem rngl_lt_neq :
  rngl_is_ordered T = true →
  ∀ a b, (a < b)%L → a ≠ b.

Theorem rngl_le_inv_inv :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < a)%L → (0 < b)%L → (a⁻¹ ≤ b⁻¹)%L ↔ (b ≤ a)%L.
Theorem rngl_div_nonneg :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → 0 < b → 0 ≤ a / b)%L.

Theorem rngl_div_pos :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < a)%L → (0 < b)%L → (0 < a / b)%L.

Theorem rngl_le_div_l :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 < c → a ≤ b × c ↔ a / c ≤ b)%L.
Theorem rngl_lt_div_l :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 < c → a < b × c ↔ a / c < b)%L.
Theorem rngl_le_div_r :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 < c → a × c ≤ b ↔ a ≤ b / c)%L.
Theorem rngl_lt_div_r :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 < c → a × c < b ↔ a < b / c)%L.
Theorem rngl_middle_sub_l :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (((a + b ) / 2 - a ) = (b - a ) / 2)%L.

Theorem rngl_middle_sub_r :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (b - (a + b ) / 2 = (b - a ) / 2)%L.

Theorem rngl_abs_le_ε :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a,
  (∀ ε, (0 < ε)%L → (rngl_abs a ≤ ε)%L)
  → a = 0%L.

Theorem rngl_mul_pos_neg :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < a → b < 0 → a × b < 0)%L.
Theorem eq_rngl_add_square_0 :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (a × a + b × b = 0)%L → a = 0%L ∧ b = 0%L.
Theorem rngl_abs_mul :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (rngl_abs (a × b) = rngl_abs a × rngl_abs b)%L.

Theorem eq_rngl_squ_rngl_abs :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  (rngl_is_integral_domain T || rngl_has_inv_or_pdiv T)%bool = true →
  ∀ a b,
  (a × b = b × a)%L
  → (a ² = b ²)%L
  → rngl_abs a = rngl_abs b.
Theorem rngl_mul_neg_neg :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (a < 0)%L → (b < 0)%L → (0 < a × b)%L.

Theorem rngl_mul_lt_mono_nonneg :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (0 ≤ a < b → 0 ≤ c < d → a × c < b × d)%L.

Theorem rngl_mul_min_distr_l :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (0 ≤ a)%L → rngl_min (a × b)%L (a × c)%L = (a × rngl_min b c)%L.

Theorem rngl_square_le_simpl_nonneg :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ b → a × a ≤ b × b → a ≤ b)%L.

Theorem rngl_pow_pos_pos :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_ordered T = true →
  ∀ a n, (0 < a → 0 < a ^ n)%L.

Theorem rngl_le_0_mul :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a × b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)%L.
Theorem rngl_abs_lt_squ_lt :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (a × b = b × a)%L → (rngl_abs a < rngl_abs b)%L → (a ² < b ²)%L.

Theorem rngl_squ_le_abs_le :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ² ≤ b ² → rngl_abs a ≤ rngl_abs b)%L.
Theorem rngl_squ_lt_abs_lt :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (a ² < b ²)%L → (rngl_abs a < rngl_abs b)%L.

Theorem rngl_squ_le_1_iff :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a, (a ² ≤ 1)%L ↔ (-1 ≤ a ≤ 1)%L.
Theorem eq_rngl_squ_0 :
  rngl_has_opp_or_psub T = true →
  (rngl_is_integral_domain T ||
     rngl_has_inv_or_pdiv T &&
     rngl_has_eq_dec_or_order T)%bool = true →
  ∀ a, (a ² = 0 → a = 0)%L.

Theorem rngl_le_squ_le :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → 0 ≤ b → a ² ≤ b ² → a ≤ b)%L.

Theorem rngl_le_le_squ :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → a ≤ b → a ² ≤ b ²)%L.

Theorem rngl_lt_squ_lt :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → 0 ≤ b → a ² < b ² → a < b)%L.

Theorem rngl_lt_lt_squ :
  rngl_has_opp T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a × b = b × a → 0 ≤ a → a < b → a ² < b ²)%L.

Theorem rngl_squ_eq_cases :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_has_eq_dec_or_order T = true →
  ∀ a b, (a × b = b × a → a ² = b ² → a = b ∨ a = -b)%L.
Theorem rngl_pow_div_pow :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ (a : T) m n,
  (a ≠ 0)%L
  → n ≤ m
  → (a ^ m / a ^ n = a ^ (m - n ))%L.

Theorem rngl_squ_inv' :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  rngl_has_eq_dec_or_order T = true →
  ∀ a, a ≠ 0%L ∨ (0⁻¹ )² = 0⁻¹ → (a⁻¹ )² = (a ² )⁻¹.

Theorem rngl_squ_div' :
  rngl_mul_is_comm T = true →
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  rngl_has_eq_dec_or_order T = true →
  ∀ a b, b ≠ 0%L ∨ (0⁻¹ )² = 0⁻¹ → (a / b )²%L = (a ² / b ²)%L.

End a.

Arguments rngl_div_le_mono_pos_l {T ro rp} Hop Hiv Hor (a b c)%_L.
Arguments rngl_div_le_mono_pos_r {T ro rp} Hop Hiv Hor (a b c)%_L.
Arguments rngl_middle_sub_r {T ro rp} Hop Hiv Hor (a b)%_L.
Arguments rngl_mul_le_mono_pos_l {T ro rp} Hop Hiq Hor (a b c)%_L.
Arguments rngl_mul_le_mono_pos_r {T ro rp} Hop Hiq Hor (a b c)%_L.
Arguments rngl_pow_div_pow {T ro rp} Hos Hiv a%_L (m n)%_nat.

This page has been generated by coqdoc