refactor(library/data/int): use "migrate" command
This commit is contained in:
Leonardo de Moura
parent
fa70930ef4
commit
d2adf922b7
2 changed files with 8 additions and 433 deletions
|
|
@ -631,156 +631,15 @@ section
|
|||
right_distrib := mul.right_distrib,
|
||||
mul_comm := mul.comm,
|
||||
eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄
|
||||
end
|
||||
|
||||
/- instantiate ring theorems to int -/
|
||||
|
||||
section port_algebra
|
||||
open [classes] algebra
|
||||
theorem mul.left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
|
||||
theorem mul.right_comm : ∀a b c : ℤ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
|
||||
theorem add.left_comm : ∀a b c : ℤ, a + (b + c) = b + (a + c) := algebra.add.left_comm
|
||||
theorem add.right_comm : ∀a b c : ℤ, (a + b) + c = (a + c) + b := algebra.add.right_comm
|
||||
theorem add.left_cancel : ∀{a b c : ℤ}, a + b = a + c → b = c := @algebra.add.left_cancel _ _
|
||||
theorem add.right_cancel : ∀{a b c : ℤ}, a + b = c + b → a = c := @algebra.add.right_cancel _ _
|
||||
theorem neg_add_cancel_left : ∀a b : ℤ, -a + (a + b) = b := algebra.neg_add_cancel_left
|
||||
theorem neg_add_cancel_right : ∀a b : ℤ, a + -b + b = a := algebra.neg_add_cancel_right
|
||||
theorem neg_eq_of_add_eq_zero : ∀{a b : ℤ}, a + b = 0 → -a = b :=
|
||||
@algebra.neg_eq_of_add_eq_zero _ _
|
||||
theorem neg_zero : -0 = 0 := algebra.neg_zero
|
||||
theorem neg_neg : ∀a : ℤ, -(-a) = a := algebra.neg_neg
|
||||
theorem neg.inj : ∀{a b : ℤ}, -a = -b → a = b := @algebra.neg.inj _ _
|
||||
theorem neg_eq_neg_iff_eq : ∀a b : ℤ, -a = -b ↔ a = b := algebra.neg_eq_neg_iff_eq
|
||||
theorem neg_eq_zero_iff_eq_zero : ∀a : ℤ, -a = 0 ↔ a = 0 := algebra.neg_eq_zero_iff_eq_zero
|
||||
theorem eq_neg_of_eq_neg : ∀{a b : ℤ}, a = -b → b = -a := @algebra.eq_neg_of_eq_neg _ _
|
||||
theorem eq_neg_iff_eq_neg : ∀{a b : ℤ}, a = -b ↔ b = -a := @algebra.eq_neg_iff_eq_neg _ _
|
||||
theorem add.right_inv : ∀a : ℤ, a + -a = 0 := algebra.add.right_inv
|
||||
theorem add_neg_cancel_left : ∀a b : ℤ, a + (-a + b) = b := algebra.add_neg_cancel_left
|
||||
theorem add_neg_cancel_right : ∀a b : ℤ, a + b + -b = a := algebra.add_neg_cancel_right
|
||||
theorem neg_add_rev : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add_rev
|
||||
theorem eq_add_neg_of_add_eq : ∀{a b c : ℤ}, a + c = b → a = b + -c :=
|
||||
@algebra.eq_add_neg_of_add_eq _ _
|
||||
theorem eq_neg_add_of_add_eq : ∀{a b c : ℤ}, b + a = c → a = -b + c :=
|
||||
@algebra.eq_neg_add_of_add_eq _ _
|
||||
theorem neg_add_eq_of_eq_add : ∀{a b c : ℤ}, b = a + c → -a + b = c :=
|
||||
@algebra.neg_add_eq_of_eq_add _ _
|
||||
theorem add_neg_eq_of_eq_add : ∀{a b c : ℤ}, a = c + b → a + -b = c :=
|
||||
@algebra.add_neg_eq_of_eq_add _ _
|
||||
theorem eq_add_of_add_neg_eq : ∀{a b c : ℤ}, a + -c = b → a = b + c :=
|
||||
@algebra.eq_add_of_add_neg_eq _ _
|
||||
theorem eq_add_of_neg_add_eq : ∀{a b c : ℤ}, -b + a = c → a = b + c :=
|
||||
@algebra.eq_add_of_neg_add_eq _ _
|
||||
theorem add_eq_of_eq_neg_add : ∀{a b c : ℤ}, b = -a + c → a + b = c :=
|
||||
@algebra.add_eq_of_eq_neg_add _ _
|
||||
theorem add_eq_of_eq_add_neg : ∀{a b c : ℤ}, a = c + -b → a + b = c :=
|
||||
@algebra.add_eq_of_eq_add_neg _ _
|
||||
theorem add_eq_iff_eq_neg_add : ∀a b c : ℤ, a + b = c ↔ b = -a + c :=
|
||||
@algebra.add_eq_iff_eq_neg_add _ _
|
||||
theorem add_eq_iff_eq_add_neg : ∀a b c : ℤ, a + b = c ↔ a = c + -b :=
|
||||
@algebra.add_eq_iff_eq_add_neg _ _
|
||||
definition sub (a b : ℤ) : ℤ := algebra.sub a b
|
||||
infix - := int.sub
|
||||
theorem sub_eq_add_neg : ∀a b : ℤ, a - b = a + -b := algebra.sub_eq_add_neg
|
||||
theorem sub_self : ∀a : ℤ, a - a = 0 := algebra.sub_self
|
||||
theorem sub_add_cancel : ∀a b : ℤ, a - b + b = a := algebra.sub_add_cancel
|
||||
theorem add_sub_cancel : ∀a b : ℤ, a + b - b = a := algebra.add_sub_cancel
|
||||
theorem eq_of_sub_eq_zero : ∀{a b : ℤ}, a - b = 0 → a = b := @algebra.eq_of_sub_eq_zero _ _
|
||||
theorem eq_iff_sub_eq_zero : ∀a b : ℤ, a = b ↔ a - b = 0 := algebra.eq_iff_sub_eq_zero
|
||||
theorem zero_sub : ∀a : ℤ, 0 - a = -a := algebra.zero_sub
|
||||
theorem sub_zero : ∀a : ℤ, a - 0 = a := algebra.sub_zero
|
||||
theorem sub_neg_eq_add : ∀a b : ℤ, a - (-b) = a + b := algebra.sub_neg_eq_add
|
||||
theorem neg_sub : ∀a b : ℤ, -(a - b) = b - a := algebra.neg_sub
|
||||
theorem add_sub : ∀a b c : ℤ, a + (b - c) = a + b - c := algebra.add_sub
|
||||
theorem sub_add_eq_sub_sub_swap : ∀a b c : ℤ, a - (b + c) = a - c - b :=
|
||||
algebra.sub_add_eq_sub_sub_swap
|
||||
theorem sub_eq_iff_eq_add : ∀a b c : ℤ, a - b = c ↔ a = c + b := algebra.sub_eq_iff_eq_add
|
||||
theorem eq_sub_iff_add_eq : ∀a b c : ℤ, a = b - c ↔ a + c = b := algebra.eq_sub_iff_add_eq
|
||||
theorem eq_iff_eq_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → (a = b ↔ c = d) :=
|
||||
@algebra.eq_iff_eq_of_sub_eq_sub _ _
|
||||
theorem eq_sub_of_add_eq : ∀{a b c : ℤ}, a + c = b → a = b - c := @algebra.eq_sub_of_add_eq _ _
|
||||
theorem sub_eq_of_eq_add : ∀{a b c : ℤ}, a = c + b → a - b = c := @algebra.sub_eq_of_eq_add _ _
|
||||
theorem eq_add_of_sub_eq : ∀{a b c : ℤ}, a - c = b → a = b + c := @algebra.eq_add_of_sub_eq _ _
|
||||
theorem add_eq_of_eq_sub : ∀{a b c : ℤ}, a = c - b → a + b = c := @algebra.add_eq_of_eq_sub _ _
|
||||
theorem sub_add_eq_sub_sub : ∀a b c : ℤ, a - (b + c) = a - b - c := algebra.sub_add_eq_sub_sub
|
||||
theorem neg_add_eq_sub : ∀a b : ℤ, -a + b = b - a := algebra.neg_add_eq_sub
|
||||
theorem neg_add : ∀a b : ℤ, -(a + b) = -a + -b := algebra.neg_add
|
||||
theorem sub_add_eq_add_sub : ∀a b c : ℤ, a - b + c = a + c - b := algebra.sub_add_eq_add_sub
|
||||
theorem sub_sub_ : ∀a b c : ℤ, a - b - c = a - (b + c) := algebra.sub_sub
|
||||
theorem add_sub_add_left_eq_sub : ∀a b c : ℤ, (c + a) - (c + b) = a - b :=
|
||||
algebra.add_sub_add_left_eq_sub
|
||||
theorem eq_sub_of_add_eq' : ∀{a b c : ℤ}, c + a = b → a = b - c := @algebra.eq_sub_of_add_eq' _ _
|
||||
theorem sub_eq_of_eq_add' : ∀{a b c : ℤ}, a = b + c → a - b = c := @algebra.sub_eq_of_eq_add' _ _
|
||||
theorem eq_add_of_sub_eq' : ∀{a b c : ℤ}, a - b = c → a = b + c := @algebra.eq_add_of_sub_eq' _ _
|
||||
theorem add_eq_of_eq_sub' : ∀{a b c : ℤ}, b = c - a → a + b = c := @algebra.add_eq_of_eq_sub' _ _
|
||||
theorem ne_zero_of_mul_ne_zero_right : ∀{a b : ℤ}, a * b ≠ 0 → a ≠ 0 :=
|
||||
@algebra.ne_zero_of_mul_ne_zero_right _ _
|
||||
theorem ne_zero_of_mul_ne_zero_left : ∀{a b : ℤ}, a * b ≠ 0 → b ≠ 0 :=
|
||||
@algebra.ne_zero_of_mul_ne_zero_left _ _
|
||||
definition dvd (a b : ℤ) : Prop := algebra.dvd a b
|
||||
notation a ∣ b := dvd a b
|
||||
theorem dvd.intro : ∀{a b c : ℤ} (H : a * c = b), a ∣ b := @algebra.dvd.intro _ _
|
||||
theorem dvd.intro_left : ∀{a b c : ℤ} (H : c * a = b), a ∣ b := @algebra.dvd.intro_left _ _
|
||||
theorem exists_eq_mul_right_of_dvd : ∀{a b : ℤ} (H : a ∣ b), ∃c, b = a * c :=
|
||||
@algebra.exists_eq_mul_right_of_dvd _ _
|
||||
theorem dvd.elim : ∀{P : Prop} {a b : ℤ} (H₁ : a ∣ b) (H₂ : ∀c, b = a * c → P), P :=
|
||||
@algebra.dvd.elim _ _
|
||||
theorem exists_eq_mul_left_of_dvd : ∀{a b : ℤ} (H : a ∣ b), ∃c, b = c * a :=
|
||||
@algebra.exists_eq_mul_left_of_dvd _ _
|
||||
theorem dvd.elim_left : ∀{P : Prop} {a b : ℤ} (H₁ : a ∣ b) (H₂ : ∀c, b = c * a → P), P :=
|
||||
@algebra.dvd.elim_left _ _
|
||||
theorem dvd.refl : ∀a : ℤ, (a ∣ a) := algebra.dvd.refl
|
||||
theorem dvd.trans : ∀{a b c : ℤ} (H₁ : a ∣ b) (H₂ : b ∣ c), a ∣ c := @algebra.dvd.trans _ _
|
||||
theorem eq_zero_of_zero_dvd : ∀{a : ℤ} (H : 0 ∣ a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
|
||||
theorem dvd_zero : ∀a : ℤ, a ∣ 0 := algebra.dvd_zero
|
||||
theorem one_dvd : ∀a : ℤ, 1 ∣ a := algebra.one_dvd
|
||||
theorem dvd_mul_right : ∀a b : ℤ, a ∣ a * b := algebra.dvd_mul_right
|
||||
theorem dvd_mul_left : ∀a b : ℤ, a ∣ b * a := algebra.dvd_mul_left
|
||||
theorem dvd_mul_of_dvd_left : ∀{a b : ℤ} (H : a ∣ b) (c : ℤ), a ∣ b * c :=
|
||||
@algebra.dvd_mul_of_dvd_left _ _
|
||||
theorem dvd_mul_of_dvd_right : ∀{a b : ℤ} (H : a ∣ b) (c : ℤ), a ∣ c * b :=
|
||||
@algebra.dvd_mul_of_dvd_right _ _
|
||||
theorem mul_dvd_mul : ∀{a b c d : ℤ}, a ∣ b → c ∣ d → a * c ∣ b * d :=
|
||||
@algebra.mul_dvd_mul _ _
|
||||
theorem dvd_of_mul_right_dvd : ∀{a b c : ℤ}, a * b ∣ c → a ∣ c :=
|
||||
@algebra.dvd_of_mul_right_dvd _ _
|
||||
theorem dvd_of_mul_left_dvd : ∀{a b c : ℤ}, a * b ∣ c → b ∣ c :=
|
||||
@algebra.dvd_of_mul_left_dvd _ _
|
||||
theorem dvd_add : ∀{a b c : ℤ}, a ∣ b → a ∣ c → a ∣ b + c := @algebra.dvd_add _ _
|
||||
theorem zero_mul : ∀a : ℤ, 0 * a = 0 := algebra.zero_mul
|
||||
theorem mul_zero : ∀a : ℤ, a * 0 = 0 := algebra.mul_zero
|
||||
theorem neg_mul_eq_neg_mul : ∀a b : ℤ, -(a * b) = -a * b := algebra.neg_mul_eq_neg_mul
|
||||
theorem neg_mul_eq_mul_neg : ∀a b : ℤ, -(a * b) = a * -b := algebra.neg_mul_eq_mul_neg
|
||||
theorem neg_mul_neg : ∀a b : ℤ, -a * -b = a * b := algebra.neg_mul_neg
|
||||
theorem neg_mul_comm : ∀a b : ℤ, -a * b = a * -b := algebra.neg_mul_comm
|
||||
theorem neg_eq_neg_one_mul : ∀a : ℤ, -a = -1 * a := algebra.neg_eq_neg_one_mul
|
||||
theorem mul_sub_left_distrib : ∀a b c : ℤ, a * (b - c) = a * b - a * c :=
|
||||
algebra.mul_sub_left_distrib
|
||||
theorem mul_sub_right_distrib : ∀a b c : ℤ, (a - b) * c = a * c - b * c :=
|
||||
algebra.mul_sub_right_distrib
|
||||
theorem mul_add_eq_mul_add_iff_sub_mul_add_eq :
|
||||
∀a b c d e : ℤ, a * e + c = b * e + d ↔ (a - b) * e + c = d :=
|
||||
algebra.mul_add_eq_mul_add_iff_sub_mul_add_eq
|
||||
theorem mul_self_sub_mul_self_eq : ∀a b : ℤ, a * a - b * b = (a + b) * (a - b) :=
|
||||
algebra.mul_self_sub_mul_self_eq
|
||||
theorem mul_self_sub_one_eq : ∀a : ℤ, a * a - 1 = (a + 1) * (a - 1) :=
|
||||
algebra.mul_self_sub_one_eq
|
||||
theorem dvd_neg_iff_dvd : ∀a b : ℤ, a ∣ -b ↔ a ∣ b := algebra.dvd_neg_iff_dvd
|
||||
theorem neg_dvd_iff_dvd : ∀a b : ℤ, -a ∣ b ↔ a ∣ b := algebra.neg_dvd_iff_dvd
|
||||
theorem dvd_sub : ∀a b c : ℤ, a ∣ b → a ∣ c → a ∣ b - c := algebra.dvd_sub
|
||||
theorem mul_ne_zero : ∀{a b : ℤ}, a ≠ 0 → b ≠ 0 → a * b ≠ 0 := @algebra.mul_ne_zero _ _
|
||||
theorem mul.cancel_right : ∀{a b c : ℤ}, a ≠ 0 → b * a = c * a → b = c :=
|
||||
@algebra.mul.cancel_right _ _
|
||||
theorem mul.cancel_left : ∀{a b c : ℤ}, a ≠ 0 → a * b = a * c → b = c :=
|
||||
@algebra.mul.cancel_left _ _
|
||||
theorem mul_self_eq_mul_self_iff : ∀a b : ℤ, a * a = b * b ↔ a = b ∨ a = -b :=
|
||||
algebra.mul_self_eq_mul_self_iff
|
||||
theorem mul_self_eq_one_iff : ∀a : ℤ, a * a = 1 ↔ a = 1 ∨ a = -1 :=
|
||||
algebra.mul_self_eq_one_iff
|
||||
theorem dvd_of_mul_dvd_mul_left : ∀{a b c : ℤ}, a ≠ 0 → a*b ∣ a*c → b ∣ c :=
|
||||
@algebra.dvd_of_mul_dvd_mul_left _ _
|
||||
theorem dvd_of_mul_dvd_mul_right : ∀{a b c : ℤ}, a ≠ 0 → b*a ∣ c*a → b ∣ c :=
|
||||
@algebra.dvd_of_mul_dvd_mul_right _ _
|
||||
end port_algebra
|
||||
|
||||
migrate from algebra with int
|
||||
replacing sub → sub, dvd → dvd
|
||||
end
|
||||
|
||||
/- additional properties -/
|
||||
|
||||
|
|
|
|||
|
|
@ -242,306 +242,22 @@ section
|
|||
⦃algebra.decidable_linear_ordered_comm_ring,
|
||||
int.linear_ordered_comm_ring,
|
||||
decidable_lt := decidable_lt⦄
|
||||
end
|
||||
|
||||
/- instantiate ordered ring theorems to int -/
|
||||
|
||||
section port_algebra
|
||||
open [classes] algebra
|
||||
definition ge [reducible] (a b : ℤ) := algebra.has_le.ge a b
|
||||
definition gt [reducible] (a b : ℤ) := algebra.has_lt.gt a b
|
||||
infix >= := int.ge
|
||||
infix ≥ := int.ge
|
||||
infix > := int.gt
|
||||
|
||||
definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) :=
|
||||
show decidable (b ≤ a), from _
|
||||
definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) :=
|
||||
show decidable (b < a), from _
|
||||
|
||||
theorem ge.trans: ∀{a b c : ℤ}, a ≥ b → b ≥ c → a ≥ c := @algebra.ge.trans _ _
|
||||
theorem gt.trans: ∀{a b c : ℤ}, a > b → b > c → a > c := @algebra.gt.trans _ _
|
||||
theorem ne_of_gt: ∀{a b : ℤ}, a > b → a ≠ b := @algebra.ne_of_gt _ _
|
||||
theorem gt_of_gt_of_ge : ∀{a b c : ℤ}, a > b → b ≥ c → a > c := @algebra.gt_of_gt_of_ge _ _
|
||||
theorem gt_of_ge_of_gt : ∀{a b c : ℤ}, a ≥ b → b > c → a > c := @algebra.gt_of_ge_of_gt _ _
|
||||
theorem lt.asymm : ∀{a b : ℤ}, a < b → ¬ b < a := @algebra.lt.asymm _ _
|
||||
theorem lt_of_le_of_ne : ∀{a b : ℤ}, a ≤ b → a ≠ b → a < b := @algebra.lt_of_le_of_ne _ _
|
||||
theorem lt_of_lt_of_le : ∀{a b c : ℤ}, a < b → b ≤ c → a < c := @algebra.lt_of_lt_of_le _ _
|
||||
theorem lt_of_le_of_lt : ∀{a b c : ℤ}, a ≤ b → b < c → a < c := @algebra.lt_of_le_of_lt _ _
|
||||
theorem not_le_of_lt : ∀{a b : ℤ}, a < b → ¬ b ≤ a := @algebra.not_le_of_lt _ _
|
||||
theorem not_lt_of_le : ∀{a b : ℤ}, a ≤ b → ¬ b < a := @algebra.not_lt_of_le _ _
|
||||
|
||||
theorem lt_or_eq_of_le : ∀{a b : ℤ}, a ≤ b → a < b ∨ a = b := @algebra.lt_or_eq_of_le _ _
|
||||
theorem lt.trichotomy : ∀a b : ℤ, a < b ∨ a = b ∨ b < a := algebra.lt.trichotomy
|
||||
theorem lt.by_cases : ∀{a b : ℤ} {P : Prop}, (a < b → P) → (a = b → P) → (b < a → P) → P :=
|
||||
@algebra.lt.by_cases _ _
|
||||
theorem le_of_not_lt : ∀{a b : ℤ}, ¬ a < b → b ≤ a := @algebra.le_of_not_lt _ _
|
||||
theorem lt_of_not_le : ∀{a b : ℤ}, ¬ a ≤ b → b < a := @algebra.lt_of_not_le _ _
|
||||
theorem lt_or_ge : ∀a b : ℤ, a < b ∨ a ≥ b := @algebra.lt_or_ge _ _
|
||||
theorem le_or_gt : ∀a b : ℤ, a ≤ b ∨ a > b := @algebra.le_or_gt _ _
|
||||
theorem lt_or_gt_of_ne : ∀{a b : ℤ}, a ≠ b → a < b ∨ a > b := @algebra.lt_or_gt_of_ne _ _
|
||||
|
||||
theorem add_le_add_right : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, a + c ≤ b + c :=
|
||||
@algebra.add_le_add_right _ _
|
||||
theorem add_le_add : ∀{a b c d : ℤ}, a ≤ b → c ≤ d → a + c ≤ b + d := @algebra.add_le_add _ _
|
||||
theorem add_lt_add_left : ∀{a b : ℤ}, a < b → ∀c : ℤ, c + a < c + b :=
|
||||
@algebra.add_lt_add_left _ _
|
||||
theorem add_lt_add_right : ∀{a b : ℤ}, a < b → ∀c : ℤ, a + c < b + c :=
|
||||
@algebra.add_lt_add_right _ _
|
||||
theorem le_add_of_nonneg_right : ∀{a b : ℤ}, b ≥ 0 → a ≤ a + b :=
|
||||
@algebra.le_add_of_nonneg_right _ _
|
||||
theorem le_add_of_nonneg_left : ∀{a b : ℤ}, b ≥ 0 → a ≤ b + a :=
|
||||
@algebra.le_add_of_nonneg_left _ _
|
||||
theorem add_lt_add : ∀{a b c d : ℤ}, a < b → c < d → a + c < b + d := @algebra.add_lt_add _ _
|
||||
theorem add_lt_add_of_le_of_lt : ∀{a b c d : ℤ}, a ≤ b → c < d → a + c < b + d :=
|
||||
@algebra.add_lt_add_of_le_of_lt _ _
|
||||
theorem add_lt_add_of_lt_of_le : ∀{a b c d : ℤ}, a < b → c ≤ d → a + c < b + d :=
|
||||
@algebra.add_lt_add_of_lt_of_le _ _
|
||||
theorem lt_add_of_pos_right : ∀{a b : ℤ}, b > 0 → a < a + b := @algebra.lt_add_of_pos_right _ _
|
||||
theorem lt_add_of_pos_left : ∀{a b : ℤ}, b > 0 → a < b + a := @algebra.lt_add_of_pos_left _ _
|
||||
theorem le_of_add_le_add_left : ∀{a b c : ℤ}, a + b ≤ a + c → b ≤ c :=
|
||||
@algebra.le_of_add_le_add_left _ _
|
||||
theorem le_of_add_le_add_right : ∀{a b c : ℤ}, a + b ≤ c + b → a ≤ c :=
|
||||
@algebra.le_of_add_le_add_right _ _
|
||||
theorem lt_of_add_lt_add_left : ∀{a b c : ℤ}, a + b < a + c → b < c :=
|
||||
@algebra.lt_of_add_lt_add_left _ _
|
||||
theorem lt_of_add_lt_add_right : ∀{a b c : ℤ}, a + b < c + b → a < c :=
|
||||
@algebra.lt_of_add_lt_add_right _ _
|
||||
theorem add_le_add_left_iff : ∀a b c : ℤ, a + b ≤ a + c ↔ b ≤ c := algebra.add_le_add_left_iff
|
||||
theorem add_le_add_right_iff : ∀a b c : ℤ, a + b ≤ c + b ↔ a ≤ c := algebra.add_le_add_right_iff
|
||||
theorem add_lt_add_left_iff : ∀a b c : ℤ, a + b < a + c ↔ b < c := algebra.add_lt_add_left_iff
|
||||
theorem add_lt_add_right_iff : ∀a b c : ℤ, a + b < c + b ↔ a < c := algebra.add_lt_add_right_iff
|
||||
theorem add_nonneg : ∀{a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b := @algebra.add_nonneg _ _
|
||||
theorem add_pos : ∀{a b : ℤ}, 0 < a → 0 < b → 0 < a + b := @algebra.add_pos _ _
|
||||
theorem add_pos_of_pos_of_nonneg : ∀{a b : ℤ}, 0 < a → 0 ≤ b → 0 < a + b :=
|
||||
@algebra.add_pos_of_pos_of_nonneg _ _
|
||||
theorem add_pos_of_nonneg_of_pos : ∀{a b : ℤ}, 0 ≤ a → 0 < b → 0 < a + b :=
|
||||
@algebra.add_pos_of_nonneg_of_pos _ _
|
||||
theorem add_nonpos : ∀{a b : ℤ}, a ≤ 0 → b ≤ 0 → a + b ≤ 0 :=
|
||||
@algebra.add_nonpos _ _
|
||||
theorem add_neg : ∀{a b : ℤ}, a < 0 → b < 0 → a + b < 0 :=
|
||||
@algebra.add_neg _ _
|
||||
theorem add_neg_of_neg_of_nonpos : ∀{a b : ℤ}, a < 0 → b ≤ 0 → a + b < 0 :=
|
||||
@algebra.add_neg_of_neg_of_nonpos _ _
|
||||
theorem add_neg_of_nonpos_of_neg : ∀{a b : ℤ}, a ≤ 0 → b < 0 → a + b < 0 :=
|
||||
@algebra.add_neg_of_nonpos_of_neg _ _
|
||||
theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg : ∀{a b : ℤ},
|
||||
0 ≤ a → 0 ≤ b → (a + b = 0 ↔ a = 0 ∧ b = 0) :=
|
||||
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _
|
||||
|
||||
theorem le_add_of_nonneg_of_le : ∀{a b c : ℤ}, 0 ≤ a → b ≤ c → b ≤ a + c :=
|
||||
@algebra.le_add_of_nonneg_of_le _ _
|
||||
theorem le_add_of_le_of_nonneg : ∀{a b c : ℤ}, b ≤ c → 0 ≤ a → b ≤ c + a :=
|
||||
@algebra.le_add_of_le_of_nonneg _ _
|
||||
theorem lt_add_of_pos_of_le : ∀{a b c : ℤ}, 0 < a → b ≤ c → b < a + c :=
|
||||
@algebra.lt_add_of_pos_of_le _ _
|
||||
theorem lt_add_of_le_of_pos : ∀{a b c : ℤ}, b ≤ c → 0 < a → b < c + a :=
|
||||
@algebra.lt_add_of_le_of_pos _ _
|
||||
theorem add_le_of_nonpos_of_le : ∀{a b c : ℤ}, a ≤ 0 → b ≤ c → a + b ≤ c :=
|
||||
@algebra.add_le_of_nonpos_of_le _ _
|
||||
theorem add_le_of_le_of_nonpos : ∀{a b c : ℤ}, b ≤ c → a ≤ 0 → b + a ≤ c :=
|
||||
@algebra.add_le_of_le_of_nonpos _ _
|
||||
theorem add_lt_of_neg_of_le : ∀{a b c : ℤ}, a < 0 → b ≤ c → a + b < c :=
|
||||
@algebra.add_lt_of_neg_of_le _ _
|
||||
theorem add_lt_of_le_of_neg : ∀{a b c : ℤ}, b ≤ c → a < 0 → b + a < c :=
|
||||
@algebra.add_lt_of_le_of_neg _ _
|
||||
theorem lt_add_of_nonneg_of_lt : ∀{a b c : ℤ}, 0 ≤ a → b < c → b < a + c :=
|
||||
@algebra.lt_add_of_nonneg_of_lt _ _
|
||||
theorem lt_add_of_lt_of_nonneg : ∀{a b c : ℤ}, b < c → 0 ≤ a → b < c + a :=
|
||||
@algebra.lt_add_of_lt_of_nonneg _ _
|
||||
theorem lt_add_of_pos_of_lt : ∀{a b c : ℤ}, 0 < a → b < c → b < a + c :=
|
||||
@algebra.lt_add_of_pos_of_lt _ _
|
||||
theorem lt_add_of_lt_of_pos : ∀{a b c : ℤ}, b < c → 0 < a → b < c + a :=
|
||||
@algebra.lt_add_of_lt_of_pos _ _
|
||||
theorem add_lt_of_nonpos_of_lt : ∀{a b c : ℤ}, a ≤ 0 → b < c → a + b < c :=
|
||||
@algebra.add_lt_of_nonpos_of_lt _ _
|
||||
theorem add_lt_of_lt_of_nonpos : ∀{a b c : ℤ}, b < c → a ≤ 0 → b + a < c :=
|
||||
@algebra.add_lt_of_lt_of_nonpos _ _
|
||||
theorem add_lt_of_neg_of_lt : ∀{a b c : ℤ}, a < 0 → b < c → a + b < c :=
|
||||
@algebra.add_lt_of_neg_of_lt _ _
|
||||
theorem add_lt_of_lt_of_neg : ∀{a b c : ℤ}, b < c → a < 0 → b + a < c :=
|
||||
@algebra.add_lt_of_lt_of_neg _ _
|
||||
|
||||
theorem neg_le_neg : ∀{a b : ℤ}, a ≤ b → -b ≤ -a := @algebra.neg_le_neg _ _
|
||||
theorem le_of_neg_le_neg : ∀{a b : ℤ}, -b ≤ -a → a ≤ b := @algebra.le_of_neg_le_neg _ _
|
||||
theorem neg_le_neg_iff_le : ∀a b : ℤ, -a ≤ -b ↔ b ≤ a := algebra.neg_le_neg_iff_le
|
||||
theorem nonneg_of_neg_nonpos : ∀{a : ℤ}, -a ≤ 0 → 0 ≤ a := @algebra.nonneg_of_neg_nonpos _ _
|
||||
theorem neg_nonpos_of_nonneg : ∀{a : ℤ}, 0 ≤ a → -a ≤ 0 := @algebra.neg_nonpos_of_nonneg _ _
|
||||
theorem neg_nonpos_iff_nonneg : ∀a : ℤ, -a ≤ 0 ↔ 0 ≤ a := algebra.neg_nonpos_iff_nonneg
|
||||
theorem nonpos_of_neg_nonneg : ∀{a : ℤ}, 0 ≤ -a → a ≤ 0 := @algebra.nonpos_of_neg_nonneg _ _
|
||||
theorem neg_nonneg_of_nonpos : ∀{a : ℤ}, a ≤ 0 → 0 ≤ -a := @algebra.neg_nonneg_of_nonpos _ _
|
||||
theorem neg_nonneg_iff_nonpos : ∀a : ℤ, 0 ≤ -a ↔ a ≤ 0 := algebra.neg_nonneg_iff_nonpos
|
||||
theorem neg_lt_neg : ∀{a b : ℤ}, a < b → -b < -a := @algebra.neg_lt_neg _ _
|
||||
theorem lt_of_neg_lt_neg : ∀{a b : ℤ}, -b < -a → a < b := @algebra.lt_of_neg_lt_neg _ _
|
||||
theorem neg_lt_neg_iff_lt : ∀a b : ℤ, -a < -b ↔ b < a := algebra.neg_lt_neg_iff_lt
|
||||
theorem pos_of_neg_neg : ∀{a : ℤ}, -a < 0 → 0 < a := @algebra.pos_of_neg_neg _ _
|
||||
theorem neg_neg_of_pos : ∀{a : ℤ}, 0 < a → -a < 0 := @algebra.neg_neg_of_pos _ _
|
||||
theorem neg_neg_iff_pos : ∀a : ℤ, -a < 0 ↔ 0 < a := algebra.neg_neg_iff_pos
|
||||
theorem neg_of_neg_pos : ∀{a : ℤ}, 0 < -a → a < 0 := @algebra.neg_of_neg_pos _ _
|
||||
theorem neg_pos_of_neg : ∀{a : ℤ}, a < 0 → 0 < -a := @algebra.neg_pos_of_neg _ _
|
||||
theorem neg_pos_iff_neg : ∀a : ℤ, 0 < -a ↔ a < 0 := algebra.neg_pos_iff_neg
|
||||
theorem le_neg_iff_le_neg : ∀a b : ℤ, a ≤ -b ↔ b ≤ -a := algebra.le_neg_iff_le_neg
|
||||
theorem neg_le_iff_neg_le : ∀a b : ℤ, -a ≤ b ↔ -b ≤ a := algebra.neg_le_iff_neg_le
|
||||
theorem lt_neg_iff_lt_neg : ∀a b : ℤ, a < -b ↔ b < -a := algebra.lt_neg_iff_lt_neg
|
||||
theorem neg_lt_iff_neg_lt : ∀a b : ℤ, -a < b ↔ -b < a := algebra.neg_lt_iff_neg_lt
|
||||
theorem sub_nonneg_iff_le : ∀a b : ℤ, 0 ≤ a - b ↔ b ≤ a := algebra.sub_nonneg_iff_le
|
||||
theorem sub_nonpos_iff_le : ∀a b : ℤ, a - b ≤ 0 ↔ a ≤ b := algebra.sub_nonpos_iff_le
|
||||
theorem sub_pos_iff_lt : ∀a b : ℤ, 0 < a - b ↔ b < a := algebra.sub_pos_iff_lt
|
||||
theorem sub_neg_iff_lt : ∀a b : ℤ, a - b < 0 ↔ a < b := algebra.sub_neg_iff_lt
|
||||
theorem add_le_iff_le_neg_add : ∀a b c : ℤ, a + b ≤ c ↔ b ≤ -a + c :=
|
||||
algebra.add_le_iff_le_neg_add
|
||||
theorem add_le_iff_le_sub_left : ∀a b c : ℤ, a + b ≤ c ↔ b ≤ c - a :=
|
||||
algebra.add_le_iff_le_sub_left
|
||||
theorem add_le_iff_le_sub_right : ∀a b c : ℤ, a + b ≤ c ↔ a ≤ c - b :=
|
||||
algebra.add_le_iff_le_sub_right
|
||||
theorem le_add_iff_neg_add_le : ∀a b c : ℤ, a ≤ b + c ↔ -b + a ≤ c :=
|
||||
algebra.le_add_iff_neg_add_le
|
||||
theorem le_add_iff_sub_left_le : ∀a b c : ℤ, a ≤ b + c ↔ a - b ≤ c :=
|
||||
algebra.le_add_iff_sub_left_le
|
||||
theorem le_add_iff_sub_right_le : ∀a b c : ℤ, a ≤ b + c ↔ a - c ≤ b :=
|
||||
algebra.le_add_iff_sub_right_le
|
||||
theorem add_lt_iff_lt_neg_add_left : ∀a b c : ℤ, a + b < c ↔ b < -a + c :=
|
||||
algebra.add_lt_iff_lt_neg_add_left
|
||||
theorem add_lt_iff_lt_neg_add_right : ∀a b c : ℤ, a + b < c ↔ a < -b + c :=
|
||||
algebra.add_lt_iff_lt_neg_add_right
|
||||
theorem add_lt_iff_lt_sub_left : ∀a b c : ℤ, a + b < c ↔ b < c - a :=
|
||||
algebra.add_lt_iff_lt_sub_left
|
||||
theorem add_lt_add_iff_lt_sub_right : ∀a b c : ℤ, a + b < c ↔ a < c - b :=
|
||||
algebra.add_lt_add_iff_lt_sub_right
|
||||
theorem lt_add_iff_neg_add_lt_left : ∀a b c : ℤ, a < b + c ↔ -b + a < c :=
|
||||
algebra.lt_add_iff_neg_add_lt_left
|
||||
theorem lt_add_iff_neg_add_lt_right : ∀a b c : ℤ, a < b + c ↔ -c + a < b :=
|
||||
algebra.lt_add_iff_neg_add_lt_right
|
||||
theorem lt_add_iff_sub_lt_left : ∀a b c : ℤ, a < b + c ↔ a - b < c :=
|
||||
algebra.lt_add_iff_sub_lt_left
|
||||
theorem lt_add_iff_sub_lt_right : ∀a b c : ℤ, a < b + c ↔ a - c < b :=
|
||||
algebra.lt_add_iff_sub_lt_right
|
||||
theorem le_iff_le_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → (a ≤ b ↔ c ≤ d) :=
|
||||
@algebra.le_iff_le_of_sub_eq_sub _ _
|
||||
theorem lt_iff_lt_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → (a < b ↔ c < d) :=
|
||||
@algebra.lt_iff_lt_of_sub_eq_sub _ _
|
||||
theorem sub_le_sub_left : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, c - b ≤ c - a :=
|
||||
@algebra.sub_le_sub_left _ _
|
||||
theorem sub_le_sub_right : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, a - c ≤ b - c :=
|
||||
@algebra.sub_le_sub_right _ _
|
||||
theorem sub_le_sub : ∀{a b c d : ℤ}, a ≤ b → c ≤ d → a - d ≤ b - c :=
|
||||
@algebra.sub_le_sub _ _
|
||||
theorem sub_lt_sub_left : ∀{a b : ℤ}, a < b → ∀c : ℤ, c - b < c - a :=
|
||||
@algebra.sub_lt_sub_left _ _
|
||||
theorem sub_lt_sub_right : ∀{a b : ℤ}, a < b → ∀c : ℤ, a - c < b - c :=
|
||||
@algebra.sub_lt_sub_right _ _
|
||||
theorem sub_lt_sub : ∀{a b c d : ℤ}, a < b → c < d → a - d < b - c :=
|
||||
@algebra.sub_lt_sub _ _
|
||||
theorem sub_lt_sub_of_le_of_lt : ∀{a b c d : ℤ}, a ≤ b → c < d → a - d < b - c :=
|
||||
@algebra.sub_lt_sub_of_le_of_lt _ _
|
||||
theorem sub_lt_sub_of_lt_of_le : ∀{a b c d : ℤ}, a < b → c ≤ d → a - d < b - c :=
|
||||
@algebra.sub_lt_sub_of_lt_of_le _ _
|
||||
theorem sub_le_self : ∀(a : ℤ) {b : ℤ}, b ≥ 0 → a - b ≤ a := algebra.sub_le_self
|
||||
theorem sub_lt_self : ∀(a : ℤ) {b : ℤ}, b > 0 → a - b < a := algebra.sub_lt_self
|
||||
|
||||
theorem eq_zero_of_neg_eq : ∀{a : ℤ}, -a = a → a = 0 := @algebra.eq_zero_of_neg_eq _ _
|
||||
definition sign : ∀a : ℤ, ℤ := algebra.sign
|
||||
definition abs : ℤ → ℤ := algebra.abs
|
||||
|
||||
theorem abs_of_nonneg : ∀{a : ℤ}, a ≥ 0 → abs a = a := @algebra.abs_of_nonneg _ _
|
||||
theorem abs_of_pos : ∀{a : ℤ}, a > 0 → abs a = a := @algebra.abs_of_pos _ _
|
||||
theorem abs_of_neg : ∀{a : ℤ}, a < 0 → abs a = -a := @algebra.abs_of_neg _ _
|
||||
theorem abs_zero : abs 0 = 0 := algebra.abs_zero
|
||||
theorem abs_of_nonpos : ∀{a : ℤ}, a ≤ 0 → abs a = -a := @algebra.abs_of_nonpos _ _
|
||||
theorem abs_neg : ∀a : ℤ, abs (-a) = abs a := algebra.abs_neg
|
||||
theorem abs_nonneg : ∀a : ℤ, abs a ≥ 0 := algebra.abs_nonneg
|
||||
theorem abs_abs : ∀a : ℤ, abs (abs a) = abs a := algebra.abs_abs
|
||||
theorem le_abs_self : ∀a : ℤ, a ≤ abs a := algebra.le_abs_self
|
||||
theorem neg_le_abs_self : ∀a : ℤ, -a ≤ abs a := algebra.neg_le_abs_self
|
||||
theorem eq_zero_of_abs_eq_zero : ∀{a : ℤ}, abs a = 0 → a = 0 := @algebra.eq_zero_of_abs_eq_zero _ _
|
||||
theorem abs_eq_zero_iff_eq_zero : ∀a : ℤ, abs a = 0 ↔ a = 0 := algebra.abs_eq_zero_iff_eq_zero
|
||||
theorem abs_pos_of_pos : ∀{a : ℤ}, a > 0 → abs a > 0 := @algebra.abs_pos_of_pos _ _
|
||||
theorem abs_pos_of_neg : ∀{a : ℤ}, a < 0 → abs a > 0 := @algebra.abs_pos_of_neg _ _
|
||||
theorem abs_pos_of_ne_zero : ∀{a : ℤ}, a ≠ 0 → abs a > 0 := @algebra.abs_pos_of_ne_zero _ _
|
||||
theorem abs_sub : ∀a b : ℤ, abs (a - b) = abs (b - a) := algebra.abs_sub
|
||||
theorem abs.by_cases : ∀{P : ℤ → Prop}, ∀{a : ℤ}, P a → P (-a) → P (abs a) :=
|
||||
@algebra.abs.by_cases _ _
|
||||
theorem abs_le_of_le_of_neg_le : ∀{a b : ℤ}, a ≤ b → -a ≤ b → abs a ≤ b :=
|
||||
@algebra.abs_le_of_le_of_neg_le _ _
|
||||
theorem abs_lt_of_lt_of_neg_lt : ∀{a b : ℤ}, a < b → -a < b → abs a < b :=
|
||||
@algebra.abs_lt_of_lt_of_neg_lt _ _
|
||||
theorem abs_add_le_abs_add_abs : ∀a b : ℤ, abs (a + b) ≤ abs a + abs b :=
|
||||
algebra.abs_add_le_abs_add_abs
|
||||
theorem abs_sub_abs_le_abs_sub : ∀a b : ℤ, abs a - abs b ≤ abs (a - b) :=
|
||||
algebra.abs_sub_abs_le_abs_sub
|
||||
|
||||
theorem mul_le_mul_of_nonneg_left : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → c * a ≤ c * b :=
|
||||
@algebra.mul_le_mul_of_nonneg_left _ _
|
||||
theorem mul_le_mul_of_nonneg_right : ∀{a b c : ℤ}, a ≤ b → 0 ≤ c → a * c ≤ b * c :=
|
||||
@algebra.mul_le_mul_of_nonneg_right _ _
|
||||
theorem mul_le_mul : ∀{a b c d : ℤ}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d :=
|
||||
@algebra.mul_le_mul _ _
|
||||
theorem mul_nonpos_of_nonneg_of_nonpos : ∀{a b : ℤ}, a ≥ 0 → b ≤ 0 → a * b ≤ 0 :=
|
||||
@algebra.mul_nonpos_of_nonneg_of_nonpos _ _
|
||||
theorem mul_nonpos_of_nonpos_of_nonneg : ∀{a b : ℤ}, a ≤ 0 → b ≥ 0 → a * b ≤ 0 :=
|
||||
@algebra.mul_nonpos_of_nonpos_of_nonneg _ _
|
||||
theorem mul_lt_mul_of_pos_left : ∀{a b c : ℤ}, a < b → 0 < c → c * a < c * b :=
|
||||
@algebra.mul_lt_mul_of_pos_left _ _
|
||||
theorem mul_lt_mul_of_pos_right : ∀{a b c : ℤ}, a < b → 0 < c → a * c < b * c :=
|
||||
@algebra.mul_lt_mul_of_pos_right _ _
|
||||
theorem mul_lt_mul : ∀{a b c d : ℤ}, a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d :=
|
||||
@algebra.mul_lt_mul _ _
|
||||
theorem mul_neg_of_pos_of_neg : ∀{a b : ℤ}, a > 0 → b < 0 → a * b < 0 :=
|
||||
@algebra.mul_neg_of_pos_of_neg _ _
|
||||
theorem mul_neg_of_neg_of_pos : ∀{a b : ℤ}, a < 0 → b > 0 → a * b < 0 :=
|
||||
@algebra.mul_neg_of_neg_of_pos _ _
|
||||
theorem lt_of_mul_lt_mul_left : ∀{a b c : ℤ}, c * a < c * b → c ≥ 0 → a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_left _ _
|
||||
theorem lt_of_mul_lt_mul_right : ∀{a b c : ℤ}, a * c < b * c → c ≥ 0 → a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_right _ _
|
||||
theorem le_of_mul_le_mul_left : ∀{a b c : ℤ}, c * a ≤ c * b → c > 0 → a ≤ b :=
|
||||
@algebra.le_of_mul_le_mul_left _ _
|
||||
theorem le_of_mul_le_mul_right : ∀{a b c : ℤ}, a * c ≤ b * c → c > 0 → a ≤ b :=
|
||||
@algebra.le_of_mul_le_mul_right _ _
|
||||
theorem pos_of_mul_pos_left : ∀{a b : ℤ}, 0 < a * b → 0 ≤ a → 0 < b :=
|
||||
@algebra.pos_of_mul_pos_left _ _
|
||||
theorem pos_of_mul_pos_right : ∀{a b : ℤ}, 0 < a * b → 0 ≤ b → 0 < a :=
|
||||
@algebra.pos_of_mul_pos_right _ _
|
||||
|
||||
theorem mul_le_mul_of_nonpos_left : ∀{a b c : ℤ}, b ≤ a → c ≤ 0 → c * a ≤ c * b :=
|
||||
@algebra.mul_le_mul_of_nonpos_left _ _
|
||||
theorem mul_le_mul_of_nonpos_right : ∀{a b c : ℤ}, b ≤ a → c ≤ 0 → a * c ≤ b * c :=
|
||||
@algebra.mul_le_mul_of_nonpos_right _ _
|
||||
theorem mul_nonneg_of_nonpos_of_nonpos : ∀{a b : ℤ}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b :=
|
||||
@algebra.mul_nonneg_of_nonpos_of_nonpos _ _
|
||||
theorem mul_lt_mul_of_neg_left : ∀{a b c : ℤ}, b < a → c < 0 → c * a < c * b :=
|
||||
@algebra.mul_lt_mul_of_neg_left _ _
|
||||
theorem mul_lt_mul_of_neg_right : ∀{a b c : ℤ}, b < a → c < 0 → a * c < b * c :=
|
||||
@algebra.mul_lt_mul_of_neg_right _ _
|
||||
theorem mul_pos_of_neg_of_neg : ∀{a b : ℤ}, a < 0 → b < 0 → 0 < a * b :=
|
||||
@algebra.mul_pos_of_neg_of_neg _ _
|
||||
|
||||
theorem mul_self_nonneg : ∀a : ℤ, a * a ≥ 0 := algebra.mul_self_nonneg
|
||||
theorem zero_le_one : #int 0 ≤ 1 := trivial
|
||||
theorem zero_lt_one : #int 0 < 1 := trivial
|
||||
theorem pos_and_pos_or_neg_and_neg_of_mul_pos : ∀{a b : ℤ}, a * b > 0 →
|
||||
(a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) := @algebra.pos_and_pos_or_neg_and_neg_of_mul_pos _ _
|
||||
|
||||
definition sign : ∀a : ℤ, ℤ := algebra.sign
|
||||
theorem sign_of_neg : ∀{a : ℤ}, a < 0 → sign a = -1 := @algebra.sign_of_neg _ _
|
||||
theorem sign_zero : sign 0 = 0 := algebra.sign_zero
|
||||
theorem sign_of_pos : ∀{a : ℤ}, a > 0 → sign a = 1 := @algebra.sign_of_pos _ _
|
||||
theorem sign_one : sign 1 = 1 := algebra.sign_one
|
||||
theorem sign_neg_one : sign (-1) = -1 := algebra.sign_neg_one
|
||||
theorem sign_sign : ∀a : ℤ, sign (sign a) = sign a := algebra.sign_sign
|
||||
theorem pos_of_sign_eq_one : ∀{a : ℤ}, sign a = 1 → a > 0 := @algebra.pos_of_sign_eq_one _ _
|
||||
theorem eq_zero_of_sign_eq_zero : ∀{a : ℤ}, sign a = 0 → a = 0 :=
|
||||
@algebra.eq_zero_of_sign_eq_zero _ _
|
||||
theorem neg_of_sign_eq_neg_one : ∀{a : ℤ}, sign a = -1 → a < 0 :=
|
||||
@algebra.neg_of_sign_eq_neg_one _ _
|
||||
theorem sign_neg : ∀a : ℤ, sign (-a) = -(sign a) := algebra.sign_neg
|
||||
theorem sign_mul : ∀a b : ℤ, sign (a * b) = sign a * sign b := algebra.sign_mul
|
||||
theorem abs_eq_sign_mul : ∀a : ℤ, abs a = sign a * a := algebra.abs_eq_sign_mul
|
||||
theorem eq_sign_mul_abs : ∀a : ℤ, a = sign a * abs a := algebra.eq_sign_mul_abs
|
||||
theorem abs_dvd_iff_dvd : ∀a b : ℤ, abs a ∣ b ↔ a ∣ b := algebra.abs_dvd_iff_dvd
|
||||
theorem dvd_abs_iff : ∀a b : ℤ, a ∣ abs b ↔ a ∣ b := algebra.dvd_abs_iff
|
||||
theorem abs_mul : ∀a b : ℤ, abs (a * b) = abs a * abs b := algebra.abs_mul
|
||||
theorem abs_mul_self : ∀a : ℤ, abs a * abs a = a * a := algebra.abs_mul_self
|
||||
end port_algebra
|
||||
migrate from algebra with int
|
||||
replacing has_le.ge → ge, has_lt.gt → gt, sign → sign, abs → abs, dvd → dvd, sub → sub
|
||||
end
|
||||
|
||||
/- more facts specific to int -/
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue