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.

Require Import Stdlib.Arith.Arith.

Require Import Utf8 Structures Order Add Mul Div.
Require Import Add_with_order 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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_ordered T = true →
  ∀ a b , (rngl_abs (a × b) = rngl_abs a × rngl_abs b)%L.

Theorem rngl_abs_inv :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  rngl_is_totally_ordered T = true →
  ∀ a , a ≠ 0%L → (rngl_abs a⁻¹ = (rngl_abs a )⁻¹)%L.

Theorem eq_rngl_squ_rngl_abs :
  rngl_has_opp T = true →
  rngl_is_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_totally_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_mul_lt_mono_pos_r {T ro rp} Hop Hiq Hto (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