feat(library/data/nat/div): revise theorems, add lcm
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
855050e623
commit
8d5a7a96b6
5 changed files with 309 additions and 105 deletions
|
|
@ -71,35 +71,41 @@ section comm_semiring
|
|||
variables [s : comm_semiring A] (a b c : A)
|
||||
include s
|
||||
|
||||
definition dvd (a b : A) : Prop := ∃c, a * c = b
|
||||
definition dvd (a b : A) : Prop := ∃c, b = a * c
|
||||
infix `|` := dvd
|
||||
|
||||
theorem dvd.intro {a b c : A} (H : a * b = c) : a | c :=
|
||||
exists.intro _ H
|
||||
theorem dvd.intro {a b c : A} (H : a * c = b) : a | b :=
|
||||
exists.intro _ H⁻¹
|
||||
|
||||
theorem dvd.intro_right {a b c : A} (H : a * b = c) : b | c :=
|
||||
theorem dvd.intro_left {a b c : A} (H : c * a = b) : a | b :=
|
||||
dvd.intro (!mul.comm ▸ H)
|
||||
|
||||
theorem dvd.ex {a b : A} (H : a | b) : ∃c, a * c = b := H
|
||||
theorem exists_eq_mul_right_of_dvd {a b : A} (H : a | b) : ∃c, b = a * c := H
|
||||
|
||||
theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, a * c = b → P) : P :=
|
||||
theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = a * c → P) : P :=
|
||||
exists.elim H₁ H₂
|
||||
|
||||
theorem exists_eq_mul_left_of_dvd {a b : A} (H : a | b) : ∃c, b = c * a :=
|
||||
dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (H1 ⬝ !mul.comm))
|
||||
|
||||
theorem dvd.elim_left {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = c * a → P) : P :=
|
||||
exists.elim (exists_eq_mul_left_of_dvd H₁) (take c, assume H₃ : b = c * a, H₂ c H₃)
|
||||
|
||||
theorem dvd.refl : a | a := dvd.intro !mul_one
|
||||
|
||||
theorem dvd.trans {a b c : A} (H₁ : a | b) (H₂ : b | c) : a | c :=
|
||||
dvd.elim H₁
|
||||
(take d, assume H₃ : a * d = b,
|
||||
(take d, assume H₃ : b = a * d,
|
||||
dvd.elim H₂
|
||||
(take e, assume H₄ : b * e = c,
|
||||
@dvd.intro _ _ _ (d * e) _
|
||||
(take e, assume H₄ : c = b * e,
|
||||
dvd.intro
|
||||
(calc
|
||||
a * (d * e) = (a * d) * e : mul.assoc
|
||||
... = b * e : H₃
|
||||
... = c : H₄)))
|
||||
|
||||
theorem eq_zero_of_zero_dvd {a : A} (H : 0 | a) : a = 0 :=
|
||||
dvd.elim H (take c, assume H' : 0 * c = a, (H')⁻¹ ⬝ !zero_mul)
|
||||
dvd.elim H (take c, assume H' : a = 0 * c, H' ⬝ !zero_mul)
|
||||
|
||||
theorem dvd_zero : a | 0 := dvd.intro !mul_zero
|
||||
|
||||
|
|
@ -112,7 +118,7 @@ section comm_semiring
|
|||
theorem dvd_mul_of_dvd_left {a b : A} (H : a | b) (c : A) : a | b * c :=
|
||||
dvd.elim H
|
||||
(take d,
|
||||
assume H₁ : a * d = b,
|
||||
assume H₁ : b = a * d,
|
||||
dvd.intro
|
||||
(calc
|
||||
a * (d * c) = a * d * c : (!mul.assoc)⁻¹
|
||||
|
|
@ -123,9 +129,9 @@ section comm_semiring
|
|||
|
||||
theorem mul_dvd_mul {a b c d : A} (dvd_ab : a | b) (dvd_cd : c | d) : a * c | b * d :=
|
||||
dvd.elim dvd_ab
|
||||
(take e, assume Haeb : a * e = b,
|
||||
(take e, assume Haeb : b = a * e,
|
||||
dvd.elim dvd_cd
|
||||
(take f, assume Hcfd : c * f = d,
|
||||
(take f, assume Hcfd : d = c * f,
|
||||
dvd.intro
|
||||
(calc
|
||||
a * c * (e * f) = a * (c * (e * f)) : mul.assoc
|
||||
|
|
@ -135,17 +141,17 @@ section comm_semiring
|
|||
... = b * d : Hcfd)))
|
||||
|
||||
theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b | c) : a | c :=
|
||||
dvd.elim H (take d, assume Habdc : a * b * d = c, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc))
|
||||
dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))
|
||||
|
||||
theorem dvd_of_mul_left_dvd {a b c : A} (H : a * b | c) : b | c :=
|
||||
dvd_of_mul_right_dvd (mul.comm a b ▸ H)
|
||||
|
||||
theorem dvd_add {a b c : A} (Hab : a | b) (Hac : a | c) : a | b + c :=
|
||||
dvd.elim Hab
|
||||
(take d, assume Hadb : a * d = b,
|
||||
(take d, assume Hadb : b = a * d,
|
||||
dvd.elim Hac
|
||||
(take e, assume Haec : a * e = c,
|
||||
dvd.intro (show a * (d + e) = b + c, from Hadb ▸ Haec ▸ left_distrib a d e)))
|
||||
(take e, assume Haec : c = a * e,
|
||||
dvd.intro (show a * (d + e) = b + c, from Hadb⁻¹ ▸ Haec⁻¹ ▸ left_distrib a d e)))
|
||||
end comm_semiring
|
||||
|
||||
/- ring -/
|
||||
|
|
@ -247,32 +253,32 @@ section
|
|||
iff.intro
|
||||
(assume H : a | -b,
|
||||
dvd.elim H
|
||||
(take c, assume H' : a * c = -b,
|
||||
(take c, assume H' : -b = a * c,
|
||||
dvd.intro
|
||||
(calc
|
||||
a * -c = -(a * c) : {!neg_mul_eq_mul_neg⁻¹}
|
||||
... = -(-b) : {H'}
|
||||
... = -(-b) : H'
|
||||
... = b : neg_neg)))
|
||||
(assume H : a | b,
|
||||
dvd.elim H
|
||||
(take c, assume H' : a * c = b,
|
||||
(take c, assume H' : b = a * c,
|
||||
dvd.intro
|
||||
(calc
|
||||
a * -c = -(a * c) : {!neg_mul_eq_mul_neg⁻¹}
|
||||
... = -b : {H'})))
|
||||
... = -b : H')))
|
||||
|
||||
theorem neg_dvd_iff_dvd : -a | b ↔ a | b :=
|
||||
iff.intro
|
||||
(assume H : -a | b,
|
||||
dvd.elim H
|
||||
(take c, assume H' : -a * c = b,
|
||||
(take c, assume H' : b = -a * c,
|
||||
dvd.intro
|
||||
(calc
|
||||
a * -c = -a * c : !neg_mul_comm⁻¹
|
||||
... = b : H')))
|
||||
(assume H : a | b,
|
||||
dvd.elim H
|
||||
(take c, assume H' : a * c = b,
|
||||
(take c, assume H' : b = a * c,
|
||||
dvd.intro
|
||||
(calc
|
||||
-a * -c = a * c : neg_mul_neg
|
||||
|
|
@ -326,15 +332,15 @@ section
|
|||
theorem dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : a * b | a * c) : b | c :=
|
||||
dvd.elim Hdvd
|
||||
(take d,
|
||||
assume H : a * b * d = a * c,
|
||||
have H1 : b * d = c, from mul.cancel_left Ha (mul.assoc a b d ▸ H),
|
||||
assume H : a * c = a * b * d,
|
||||
have H1 : b * d = c, from mul.cancel_left Ha (mul.assoc a b d ▸ H⁻¹),
|
||||
dvd.intro H1)
|
||||
|
||||
theorem dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : b * a | c * a) : b | c :=
|
||||
dvd.elim Hdvd
|
||||
(take d,
|
||||
assume H : b * a * d = c * a,
|
||||
have H1 : b * d * a = c * a, from eq.trans !mul.right_comm H,
|
||||
assume H : c * a = b * a * d,
|
||||
have H1 : b * d * a = c * a, from eq.trans !mul.right_comm H⁻¹,
|
||||
have H2 : b * d = c, from mul.cancel_right Ha H1,
|
||||
dvd.intro H2)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -692,11 +692,16 @@ section port_algebra
|
|||
@algebra.ne_zero_of_mul_ne_zero_left _ _
|
||||
definition dvd (a b : ℤ) : Prop := algebra.dvd a b
|
||||
infix `|` := dvd
|
||||
theorem dvd.intro : ∀{a b c : ℤ} (H : a * b = c), a | c := @algebra.dvd.intro _ _
|
||||
theorem dvd.intro_right : ∀{a b c : ℤ} (H : a * b = c), b | c := @algebra.dvd.intro_right _ _
|
||||
theorem dvd.ex : ∀{a b : ℤ} (H : a | b), ∃c, a * c = b := @algebra.dvd.ex _ _
|
||||
theorem dvd.elim : ∀{P : Prop} {a b : ℤ} (H₁ : a | b) (H₂ : ∀c, a * c = b → P), P :=
|
||||
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 _ _
|
||||
|
|
|
|||
|
|
@ -26,10 +26,16 @@ section port_algebra
|
|||
|
||||
definition dvd (a b : ℕ) : Prop := algebra.dvd a b
|
||||
infix `|` := dvd
|
||||
theorem dvd.intro : ∀{a b c : ℕ} (H : a * b = c), a | c := @algebra.dvd.intro _ _
|
||||
theorem dvd.ex : ∀{a b : ℕ} (H : a | b), ∃c, a * c = b := @algebra.dvd.ex _ _
|
||||
theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, a * c = b → P), P :=
|
||||
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 _ _
|
||||
|
|
|
|||
|
|
@ -41,16 +41,16 @@ divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_of_lt_of_le l
|
|||
theorem div_eq_succ_sub_div {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a - b) div b) :=
|
||||
divide_def a b ⬝ if_pos (and.intro h₁ h₂)
|
||||
|
||||
theorem add_div_left {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) :=
|
||||
theorem add_div_self_right (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) :=
|
||||
calc
|
||||
(x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def
|
||||
... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x))
|
||||
... = succ (x div z) : {!add_sub_cancel}
|
||||
|
||||
theorem add_div_right {x z : ℕ} (H : x > 0) : (x + z) div x = succ (z div x) :=
|
||||
!add.comm ▸ add_div_left H
|
||||
theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) div x = succ (z div x) :=
|
||||
!add.comm ▸ !add_div_self_right H
|
||||
|
||||
theorem add_mul_div_left {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y :=
|
||||
theorem add_mul_div_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y :=
|
||||
induction_on y
|
||||
(calc (x + zero * z) div z = (x + zero) div z : zero_mul
|
||||
... = x div z : add_zero
|
||||
|
|
@ -58,11 +58,21 @@ induction_on y
|
|||
(take y,
|
||||
assume IH : (x + y * z) div z = x div z + y, calc
|
||||
(x + succ y * z) div z = (x + y * z + z) div z : by simp
|
||||
... = succ ((x + y * z) div z) : add_div_left H
|
||||
... = succ ((x + y * z) div z) : !add_div_self_right H
|
||||
... = x div z + succ y : by simp)
|
||||
|
||||
theorem add_mul_div_right {x y z : ℕ} (H : y > 0) : (x + y * z) div y = x div y + z :=
|
||||
!mul.comm ▸ add_mul_div_left H
|
||||
theorem add_mul_div_self_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) div y = x div y + z :=
|
||||
!mul.comm ▸ add_mul_div_self_right H
|
||||
|
||||
theorem mul_div_self_right (m : ℕ) {n : ℕ} (H : n > 0) : m * n div n = m :=
|
||||
calc
|
||||
m * n div n = (0 + m * n) div n : zero_add
|
||||
... = 0 div n + m : add_mul_div_self_right H
|
||||
... = 0 + m : zero_div
|
||||
... = m : zero_add
|
||||
|
||||
theorem mul_div_self_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n :=
|
||||
!mul.comm ▸ !mul_div_self_right H
|
||||
|
||||
private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
|
||||
if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
|
||||
|
|
@ -95,7 +105,7 @@ calc
|
|||
theorem add_mod_right {x z : ℕ} (H : x > 0) : (x + z) mod x = z mod x :=
|
||||
!add.comm ▸ add_mod_left H
|
||||
|
||||
theorem add_mul_mod_left {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z :=
|
||||
theorem add_mul_mod_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z :=
|
||||
induction_on y
|
||||
(calc (x + zero * z) mod z = (x + zero) mod z : zero_mul
|
||||
... = x mod z : add_zero)
|
||||
|
|
@ -107,14 +117,14 @@ induction_on y
|
|||
... = (x + y * z) mod z : add_mod_left H
|
||||
... = x mod z : IH)
|
||||
|
||||
theorem add_mul_mod_right {x y z : ℕ} (H : y > 0) : (x + y * z) mod y = x mod y :=
|
||||
!mul.comm ▸ add_mul_mod_left H
|
||||
theorem add_mul_mod_self_left {x y z : ℕ} (H : y > 0) : (x + y * z) mod y = x mod y :=
|
||||
!mul.comm ▸ add_mul_mod_self_right H
|
||||
|
||||
theorem mul_mod_left {m n : ℕ} : (m * n) mod n = 0 :=
|
||||
by_cases_zero_pos n (by simp)
|
||||
(take n,
|
||||
assume npos : n > 0,
|
||||
(by simp) ▸ (@add_mul_mod_left 0 m _ npos))
|
||||
(by simp) ▸ (@add_mul_mod_self_right 0 m _ npos))
|
||||
|
||||
theorem mul_mod_right {m n : ℕ} : (m * n) mod m = 0 :=
|
||||
!mul.comm ▸ !mul_mod_left
|
||||
|
|
@ -181,10 +191,10 @@ theorem eq_remainder {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2
|
|||
(H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 :=
|
||||
calc
|
||||
r1 = r1 mod y : by simp
|
||||
... = (r1 + q1 * y) mod y : (add_mul_mod_left H)⁻¹
|
||||
... = (r1 + q1 * y) mod y : (add_mul_mod_self_right H)⁻¹
|
||||
... = (q1 * y + r1) mod y : add.comm
|
||||
... = (r2 + q2 * y) mod y : by simp
|
||||
... = r2 mod y : add_mul_mod_left H
|
||||
... = r2 mod y : add_mul_mod_self_right H
|
||||
... = r2 : by simp
|
||||
|
||||
theorem eq_quotient {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y)
|
||||
|
|
@ -194,7 +204,7 @@ have H5 : q1 * y = q2 * y, from add.cancel_right H4,
|
|||
have H6 : y > 0, from lt_of_le_of_lt !zero_le H1,
|
||||
show q1 = q2, from eq_of_mul_eq_mul_right H6 H5
|
||||
|
||||
theorem mul_div_mul_left {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
|
||||
theorem mul_div_mul_left {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y :=
|
||||
by_cases -- (y = 0)
|
||||
(assume H : y = 0, by simp)
|
||||
(assume H : y ≠ 0,
|
||||
|
|
@ -210,35 +220,43 @@ by_cases -- (y = 0)
|
|||
... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm))
|
||||
|
||||
theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) div (y * z) = x div y :=
|
||||
!mul.comm ▸ !mul.comm ▸ mul_div_mul_left zpos
|
||||
!mul.comm ▸ !mul.comm ▸ !mul_div_mul_left zpos
|
||||
|
||||
theorem mul_mod_mul_left {z x y : ℕ} (zpos : z > 0) : (z * x) mod (z * y) = z * (x mod y) :=
|
||||
by_cases -- (y = 0)
|
||||
(assume H : y = 0, by simp)
|
||||
(assume H : y ≠ 0,
|
||||
have ypos : y > 0, from pos_of_ne_zero H,
|
||||
have zypos : z * y > 0, from mul_pos zpos ypos,
|
||||
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos,
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
|
||||
eq_remainder zypos H1 H2
|
||||
(calc
|
||||
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : eq_div_mul_add_mod
|
||||
... = z * (x div y * y + x mod y) : eq_div_mul_add_mod
|
||||
... = z * (x div y * y) + z * (x mod y) : mul.left_distrib
|
||||
... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm))
|
||||
theorem mul_mod_mul_left (z x y : ℕ) : (z * x) mod (z * y) = z * (x mod y) :=
|
||||
or.elim (eq_zero_or_pos z)
|
||||
(assume H : z = 0,
|
||||
calc
|
||||
(z * x) mod (z * y) = (0 * x) mod (z * y) : H
|
||||
... = 0 mod (z * y) : zero_mul
|
||||
... = 0 : zero_mod
|
||||
... = 0 * (x mod y) : zero_mul
|
||||
... = z * (x mod y) : H)
|
||||
(assume zpos : z > 0,
|
||||
or.elim (eq_zero_or_pos y)
|
||||
(assume H : y = 0, by simp)
|
||||
(assume ypos : y > 0,
|
||||
have zypos : z * y > 0, from mul_pos zpos ypos,
|
||||
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos,
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
|
||||
eq_remainder zypos H1 H2
|
||||
(calc
|
||||
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : eq_div_mul_add_mod
|
||||
... = z * (x div y * y + x mod y) : eq_div_mul_add_mod
|
||||
... = z * (x div y * y) + z * (x mod y) : mul.left_distrib
|
||||
... = (x div y) * (z * y) + z * (x mod y) : mul.left_comm)))
|
||||
|
||||
theorem mul_mod_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) mod (y * z) = (x mod y) * z :=
|
||||
mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ mul_mod_mul_left zpos
|
||||
theorem mul_mod_mul_right (x z y : ℕ) : (x * z) mod (y * z) = (x mod y) * z :=
|
||||
mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ !mul_mod_mul_left
|
||||
|
||||
theorem mod_one (x : ℕ) : x mod 1 = 0 :=
|
||||
have H1 : x mod 1 < 1, from mod_lt !succ_pos,
|
||||
theorem mod_one (n : ℕ) : n mod 1 = 0 :=
|
||||
have H1 : n mod 1 < 1, from mod_lt !succ_pos,
|
||||
eq_zero_of_le_zero (le_of_lt_succ H1)
|
||||
|
||||
theorem mod_self (n : ℕ) : n mod n = 0 :=
|
||||
cases_on n (by simp)
|
||||
(take n,
|
||||
have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
|
||||
from mul_mod_mul_left !succ_pos,
|
||||
from !mul_mod_mul_left,
|
||||
(by simp) ▸ H)
|
||||
|
||||
theorem div_one (n : ℕ) : n div 1 = n :=
|
||||
|
|
@ -246,34 +264,40 @@ have H : n div 1 * 1 + n mod 1 = n, from eq_div_mul_add_mod⁻¹,
|
|||
(by simp) ▸ H
|
||||
|
||||
theorem div_self {n : ℕ} (H : n > 0) : n div n = 1 :=
|
||||
have H1 : (n * 1) div (n * 1) = 1 div 1, from mul_div_mul_left H,
|
||||
have H1 : (n * 1) div (n * 1) = 1 div 1, from !mul_div_mul_left H,
|
||||
(by simp) ▸ H1
|
||||
|
||||
theorem div_mul_eq_of_mod_eq_zero {x y : ℕ} (H : x mod y = 0) : x div y * y = x :=
|
||||
theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : m div n * n = m :=
|
||||
(calc
|
||||
x = x div y * y + x mod y : eq_div_mul_add_mod
|
||||
... = x div y * y + 0 : H
|
||||
... = x div y * y : !add_zero)⁻¹
|
||||
m = m div n * n + m mod n : eq_div_mul_add_mod
|
||||
... = m div n * n + 0 : H
|
||||
... = m div n * n : !add_zero)⁻¹
|
||||
|
||||
theorem mul_div_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : n * (m div n) = m :=
|
||||
!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H
|
||||
|
||||
/- divides -/
|
||||
|
||||
theorem dvd_of_mod_eq_zero {x y : ℕ} (H : y mod x = 0) : x | y :=
|
||||
dvd.intro (!mul.comm ▸ div_mul_eq_of_mod_eq_zero H)
|
||||
theorem dvd_of_mod_eq_zero {m n : ℕ} (H : n mod m = 0) : m | n :=
|
||||
dvd.intro (!mul.comm ▸ div_mul_cancel_of_mod_eq_zero H)
|
||||
|
||||
theorem mod_eq_zero_of_dvd {x y : ℕ} (H : x | y) : y mod x = 0 :=
|
||||
theorem mod_eq_zero_of_dvd {m n : ℕ} (H : m | n) : n mod m = 0 :=
|
||||
dvd.elim H
|
||||
(take z,
|
||||
assume H1 : x * z = y,
|
||||
H1 ▸ !mul_mod_right)
|
||||
assume H1 : n = m * z,
|
||||
H1⁻¹ ▸ !mul_mod_right)
|
||||
|
||||
theorem dvd_iff_mod_eq_zero (x y : ℕ) : x | y ↔ y mod x = 0 :=
|
||||
theorem dvd_iff_mod_eq_zero (m n : ℕ) : m | n ↔ n mod m = 0 :=
|
||||
iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero
|
||||
|
||||
definition dvd.decidable_rel [instance] : decidable_rel dvd :=
|
||||
take m n, decidable_of_decidable_of_iff _ (iff.symm !dvd_iff_mod_eq_zero)
|
||||
|
||||
theorem div_mul_eq_of_dvd {x y : ℕ} (H : y | x) : x div y * y = x :=
|
||||
div_mul_eq_of_mod_eq_zero (mod_eq_zero_of_dvd H)
|
||||
theorem div_mul_cancel {m n : ℕ} (H : n | m) : m div n * n = m :=
|
||||
div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H)
|
||||
|
||||
theorem mul_div_cancel {m n : ℕ} (H : n | m) : n * (m div n) = m :=
|
||||
!mul.comm ▸ div_mul_cancel H
|
||||
|
||||
theorem dvd_of_dvd_add_left {m n1 n2 : ℕ} : m | (n1 + n2) → m | n1 → m | n2 :=
|
||||
by_cases_zero_pos m
|
||||
|
|
@ -290,13 +314,13 @@ by_cases_zero_pos m
|
|||
assume H1 : m | (n1 + n2),
|
||||
assume H2 : m | n1,
|
||||
have H3 : n1 + n2 = n1 + n2 div m * m, from calc
|
||||
n1 + n2 = (n1 + n2) div m * m : div_mul_eq_of_dvd H1
|
||||
... = (n1 div m * m + n2) div m * m : div_mul_eq_of_dvd H2
|
||||
n1 + n2 = (n1 + n2) div m * m : div_mul_cancel H1
|
||||
... = (n1 div m * m + n2) div m * m : div_mul_cancel H2
|
||||
... = (n2 + n1 div m * m) div m * m : add.comm
|
||||
... = (n2 div m + n1 div m) * m : add_mul_div_left mpos
|
||||
... = (n2 div m + n1 div m) * m : add_mul_div_self_right mpos
|
||||
... = n2 div m * m + n1 div m * m : mul.right_distrib
|
||||
... = n1 div m * m + n2 div m * m : add.comm
|
||||
... = n1 + n2 div m * m : div_mul_eq_of_dvd H2,
|
||||
... = n1 + n2 div m * m : div_mul_cancel H2,
|
||||
have H4 : n2 = n2 div m * m, from add.cancel_left H3,
|
||||
have H5 : m * (n2 div m) = n2, from !mul.comm ▸ H4⁻¹,
|
||||
dvd.intro H5)
|
||||
|
|
@ -320,14 +344,35 @@ by_cases_zero_pos n
|
|||
assume Hpos : n > 0,
|
||||
assume H1 : m | n,
|
||||
assume H2 : n | m,
|
||||
obtain k (Hk : m * k = n), from dvd.ex H1,
|
||||
obtain l (Hl : n * l = m), from dvd.ex H2,
|
||||
have H3 : n * (l * k) = n, from !mul.assoc ▸ Hl⁻¹ ▸ Hk,
|
||||
obtain k (Hk : n = m * k), from exists_eq_mul_right_of_dvd H1,
|
||||
obtain l (Hl : m = n * l), from exists_eq_mul_right_of_dvd H2,
|
||||
have H3 : n * (l * k) = n, from !mul.assoc ▸ Hl ▸ Hk⁻¹,
|
||||
have H4 : l * k = 1, from eq_one_of_mul_eq_self_right Hpos H3,
|
||||
have H5 : k = 1, from eq_one_of_mul_eq_one_left H4,
|
||||
show m = n, from (mul_one m)⁻¹ ⬝ (H5 ▸ Hk))
|
||||
show m = n, from (mul_one m)⁻¹ ⬝ (H5 ▸ Hk⁻¹))
|
||||
|
||||
/- gcd and lcm -/
|
||||
theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k | n) : m * n div k = m * (n div k) :=
|
||||
or.elim (eq_zero_or_pos k)
|
||||
(assume H1 : k = 0,
|
||||
calc
|
||||
m * n div k = m * n div 0 : H1
|
||||
... = 0 : div_zero
|
||||
... = m * 0 : mul_zero m -- TODO: why do we have to specify m here?
|
||||
... = m * (n div 0) : div_zero
|
||||
... = m * (n div k) : H1)
|
||||
(assume H1 : k > 0,
|
||||
have H2 : n = n div k * k, from (div_mul_cancel H)⁻¹,
|
||||
calc
|
||||
m * n div k = m * (n div k * k) div k : H2
|
||||
... = m * (n div k) * k div k : mul.assoc
|
||||
... = m * (n div k) : mul_div_self_right _ H1)
|
||||
|
||||
theorem eq_mul_of_div_eq {m n k : ℕ} (H1 : m | n) (H2 : n div m = k) : n = m * k :=
|
||||
eq.symm (calc
|
||||
m * k = m * (n div m) : H2
|
||||
... = n : mul_div_cancel H1)
|
||||
|
||||
/- gcd -/
|
||||
|
||||
private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure pr₂
|
||||
private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
|
||||
|
|
@ -346,35 +391,32 @@ prod.cases_on p₁ (λx y, cases_on y
|
|||
|
||||
definition gcd (x y : nat) := fix gcd.F (pair x y)
|
||||
|
||||
theorem gcd_zero (x : nat) : gcd x 0 = x :=
|
||||
theorem gcd_zero_right (x : nat) : gcd x 0 = x :=
|
||||
well_founded.fix_eq gcd.F (x, 0)
|
||||
|
||||
theorem gcd_succ (x y : nat) : gcd x (succ y) = gcd (succ y) (x mod succ y) :=
|
||||
well_founded.fix_eq gcd.F (x, succ y)
|
||||
|
||||
theorem gcd_one (n : ℕ) : gcd n 1 = 1 :=
|
||||
theorem gcd_one_right (n : ℕ) : gcd n 1 = 1 :=
|
||||
calc gcd n 1 = gcd 1 (n mod 1) : gcd_succ n zero
|
||||
... = gcd 1 0 : mod_one
|
||||
... = 1 : gcd_zero
|
||||
... = 1 : gcd_zero_right
|
||||
|
||||
theorem gcd_def (x y : ℕ) : gcd x y = if y = 0 then x else gcd y (x mod y) :=
|
||||
cases_on y
|
||||
(calc gcd x 0 = x : gcd_zero x
|
||||
(calc gcd x 0 = x : gcd_zero_right x
|
||||
... = if 0 = 0 then x else gcd zero (x mod zero) : (if_pos rfl)⁻¹)
|
||||
(λy₁, calc
|
||||
gcd x (succ y₁) = gcd (succ y₁) (x mod succ y₁) : gcd_succ x y₁
|
||||
... = if succ y₁ = 0 then x else gcd (succ y₁) (x mod succ y₁) : (if_neg (succ_ne_zero y₁))⁻¹)
|
||||
|
||||
theorem gcd_rec (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) :=
|
||||
gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
|
||||
|
||||
theorem gcd_self (n : ℕ) : gcd n n = n :=
|
||||
cases_on n
|
||||
rfl
|
||||
(λn₁, calc
|
||||
gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ mod succ n₁) : gcd_succ (succ n₁) n₁
|
||||
... = gcd (succ n₁) 0 : mod_self (succ n₁)
|
||||
... = succ n₁ : gcd_zero)
|
||||
... = succ n₁ : gcd_zero_right)
|
||||
|
||||
theorem gcd_zero_left (n : nat) : gcd 0 n = n :=
|
||||
cases_on n
|
||||
|
|
@ -382,7 +424,18 @@ cases_on n
|
|||
(λ n₁, calc
|
||||
gcd 0 (succ n₁) = gcd (succ n₁) (0 mod succ n₁) : gcd_succ
|
||||
... = gcd (succ n₁) 0 : zero_mod
|
||||
... = (succ n₁) : gcd_zero)
|
||||
... = (succ n₁) : gcd_zero_right)
|
||||
|
||||
theorem gcd_rec_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) :=
|
||||
gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
|
||||
|
||||
theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m mod n) :=
|
||||
by_cases_zero_pos n
|
||||
(calc
|
||||
gcd m 0 = m : gcd_zero_right
|
||||
... = gcd 0 m : gcd_zero_left
|
||||
... = gcd 0 (m mod 0) : mod_zero)
|
||||
(take n, assume H : 0 < n, gcd_rec_of_pos m H)
|
||||
|
||||
theorem gcd.induction {P : ℕ → ℕ → Prop}
|
||||
(m n : ℕ)
|
||||
|
|
@ -412,7 +465,7 @@ gcd.induction m n
|
|||
have H : gcd n (m mod n) | (m div n * n + m mod n), from
|
||||
dvd_add (dvd.trans (and.elim_left IH) !dvd_mul_left) (and.elim_right IH),
|
||||
have H1 : gcd n (m mod n) | m, from eq_div_mul_add_mod⁻¹ ▸ H,
|
||||
have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_rec _ npos)⁻¹,
|
||||
have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹,
|
||||
show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and.elim_left IH)))
|
||||
|
||||
theorem gcd_dvd_left (m n : ℕ) : (gcd m n | m) := and.elim_left !gcd_dvd
|
||||
|
|
@ -422,7 +475,7 @@ theorem gcd_dvd_right (m n : ℕ) : (gcd m n | n) := and.elim_right !gcd_dvd
|
|||
theorem dvd_gcd {m n k : ℕ} : k | m → k | n → k | (gcd m n) :=
|
||||
gcd.induction m n
|
||||
(take m, assume (h₁ : k | m) (h₂ : k | 0),
|
||||
show k | gcd m 0, from !gcd_zero⁻¹ ▸ h₁)
|
||||
show k | gcd m 0, from !gcd_zero_right⁻¹ ▸ h₁)
|
||||
(take m n,
|
||||
assume npos : n > 0,
|
||||
assume IH : k | n → k | (m mod n) → k | gcd n (m mod n),
|
||||
|
|
@ -430,7 +483,7 @@ gcd.induction m n
|
|||
assume H2 : k | n,
|
||||
have H3 : k | m div n * n + m mod n, from eq_div_mul_add_mod ▸ H1,
|
||||
have H4 : k | m mod n, from nat.dvd_of_dvd_add_left H3 (dvd.trans H2 (by simp)),
|
||||
have gcd_eq : gcd n (m mod n) = gcd m n, from (gcd_rec _ npos)⁻¹,
|
||||
have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹,
|
||||
show k | gcd m n, from gcd_eq ▸ IH H2 H4)
|
||||
|
||||
theorem gcd.comm (m n : ℕ) : gcd m n = gcd n m :=
|
||||
|
|
@ -447,4 +500,132 @@ dvd.antisymm
|
|||
(dvd_gcd !gcd_dvd_left (dvd.trans !gcd_dvd_right !gcd_dvd_left))
|
||||
(dvd.trans !gcd_dvd_right !gcd_dvd_right))
|
||||
|
||||
theorem gcd_one_left (m : ℕ) : gcd 1 m = 1 :=
|
||||
!gcd.comm ⬝ !gcd_one_right
|
||||
|
||||
theorem gcd_mul_left (m n k : ℕ) : gcd (m * n) (m * k) = m * gcd n k :=
|
||||
gcd.induction n k
|
||||
(take n,
|
||||
calc
|
||||
gcd (m * n) (m * 0) = gcd (m * n) 0 : mul_zero
|
||||
... = m * n : gcd_zero_right
|
||||
... = m * gcd n 0 : gcd_zero_right)
|
||||
(take n k,
|
||||
assume H : 0 < k,
|
||||
assume IH : gcd (m * k) (m * (n mod k)) = m * gcd k (n mod k),
|
||||
calc
|
||||
gcd (m * n) (m * k) = gcd (m * k) (m * n mod (m * k)) : !gcd_rec
|
||||
... = gcd (m * k) (m * (n mod k)) : mul_mod_mul_left
|
||||
... = m * gcd k (n mod k) : IH
|
||||
... = m * gcd n k : !gcd_rec)
|
||||
|
||||
theorem gcd_mul_right (m n k : ℕ) : gcd (m * n) (k * n) = gcd m k * n :=
|
||||
calc
|
||||
gcd (m * n) (k * n) = gcd (n * m) (k * n) : mul.comm
|
||||
... = gcd (n * m) (n * k) : mul.comm
|
||||
... = n * gcd m k : gcd_mul_left
|
||||
... = gcd m k * n : mul.comm
|
||||
|
||||
theorem gcd_pos_of_pos_left {m : ℕ} (n : ℕ) (mpos : m > 0) : gcd m n > 0 :=
|
||||
pos_of_dvd_of_pos !gcd_dvd_left mpos
|
||||
|
||||
theorem gcd_pos_of_pos_right (m : ℕ) {n : ℕ} (npos : n > 0) : gcd m n > 0 :=
|
||||
pos_of_dvd_of_pos !gcd_dvd_right npos
|
||||
|
||||
/- lcm -/
|
||||
|
||||
definition lcm (m n : ℕ) : ℕ := m * n div (gcd m n)
|
||||
|
||||
theorem lcm.comm (m n : ℕ) : lcm m n = lcm n m :=
|
||||
calc
|
||||
lcm m n = m * n div gcd m n : rfl
|
||||
... = n * m div gcd m n : mul.comm
|
||||
... = n * m div gcd n m : gcd.comm
|
||||
... = lcm n m : rfl
|
||||
|
||||
theorem lcm_zero_left (m : ℕ) : lcm 0 m = 0 :=
|
||||
calc
|
||||
lcm 0 m = 0 * m div gcd 0 m : rfl
|
||||
... = 0 div gcd 0 m : zero_mul
|
||||
... = 0 : zero_div
|
||||
|
||||
theorem lcm_zero_right (m : ℕ) : lcm m 0 = 0 := !lcm.comm ▸ !lcm_zero_left
|
||||
|
||||
theorem lcm_one_left (m : ℕ) : lcm 1 m = m :=
|
||||
calc
|
||||
lcm 1 m = 1 * m div gcd 1 m : rfl
|
||||
... = m div gcd 1 m : one_mul
|
||||
... = m div 1 : gcd_one_left
|
||||
... = m : div_one
|
||||
|
||||
theorem lcm_one_right (m : ℕ) : lcm m 1 = m := !lcm.comm ▸ !lcm_one_left
|
||||
|
||||
theorem lcm_self (m : ℕ) : lcm m m = m :=
|
||||
have H : m * m div m = m, from
|
||||
by_cases_zero_pos m !div_zero (take m, assume H1 : m > 0, !mul_div_self_right H1),
|
||||
calc
|
||||
lcm m m = m * m div gcd m m : rfl
|
||||
... = m * m div m : gcd_self
|
||||
... = m : H
|
||||
|
||||
theorem dvd_lcm_left (m n : ℕ) : m | lcm m n :=
|
||||
have H : lcm m n = m * (n div gcd m n), from mul_div_assoc _ !gcd_dvd_right,
|
||||
dvd.intro H⁻¹
|
||||
|
||||
theorem dvd_lcm_right (m n : ℕ) : n | lcm m n :=
|
||||
!lcm.comm ▸ !dvd_lcm_left
|
||||
|
||||
theorem gcd_mul_lcm (m n : ℕ) : gcd m n * lcm m n = m * n :=
|
||||
eq.symm (eq_mul_of_div_eq (dvd.trans !gcd_dvd_left !dvd_mul_right) rfl)
|
||||
|
||||
theorem lcm_dvd {m n k : ℕ} (H1 : m | k) (H2 : n | k) : lcm m n | k :=
|
||||
or.elim (eq_zero_or_pos k)
|
||||
(assume kzero : k = 0, !kzero⁻¹ ▸ !dvd_zero)
|
||||
(assume kpos : k > 0,
|
||||
have mpos : m > 0, from pos_of_dvd_of_pos H1 kpos,
|
||||
have npos : n > 0, from pos_of_dvd_of_pos H2 kpos,
|
||||
have gcd_pos : gcd m n > 0, from !gcd_pos_of_pos_left mpos,
|
||||
obtain p (km : k = m * p), from exists_eq_mul_right_of_dvd H1,
|
||||
obtain q (kn : k = n * q), from exists_eq_mul_right_of_dvd H2,
|
||||
have ppos : p > 0, from pos_of_mul_pos_left (km ▸ kpos),
|
||||
have qpos : q > 0, from pos_of_mul_pos_left (kn ▸ kpos),
|
||||
have H3 : p * q * (m * n * gcd p q) = p * q * (gcd m n * k), from
|
||||
calc
|
||||
p * q * (m * n * gcd p q) = p * (q * (m * n * gcd p q)) : mul.assoc
|
||||
... = p * (q * (m * (n * gcd p q))) : mul.assoc
|
||||
... = p * (m * (q * (n * gcd p q))) : mul.left_comm
|
||||
... = p * m * (q * (n * gcd p q)) : mul.assoc
|
||||
... = p * m * (q * n * gcd p q) : mul.assoc
|
||||
... = m * p * (q * n * gcd p q) : mul.comm
|
||||
... = k * (q * n * gcd p q) : km
|
||||
... = k * (n * q * gcd p q) : mul.comm
|
||||
... = k * (k * gcd p q) : kn
|
||||
... = k * gcd (k * p) (k * q) : gcd_mul_left
|
||||
... = k * gcd (n * q * p) (k * q) : kn
|
||||
... = k * gcd (n * q * p) (m * p * q) : km
|
||||
... = k * gcd (n * (q * p)) (m * p * q) : mul.assoc
|
||||
... = k * gcd (n * (q * p)) (m * (p * q)) : mul.assoc
|
||||
... = k * gcd (n * (p * q)) (m * (p * q)) : mul.comm
|
||||
... = k * (gcd n m * (p * q)) : gcd_mul_right
|
||||
... = gcd n m * (p * q) * k : mul.comm
|
||||
... = p * q * gcd n m * k : mul.comm
|
||||
... = p * q * (gcd n m * k) : mul.assoc
|
||||
... = p * q * (gcd m n * k) : gcd.comm,
|
||||
have H4 : m * n * gcd p q = gcd m n * k,
|
||||
from !eq_of_mul_eq_mul_left (mul_pos ppos qpos) H3,
|
||||
have H5 : gcd m n * (lcm m n * gcd p q) = gcd m n * k,
|
||||
from !mul.assoc ▸ !gcd_mul_lcm⁻¹ ▸ H4,
|
||||
have H6 : lcm m n * gcd p q = k,
|
||||
from !eq_of_mul_eq_mul_left gcd_pos H5,
|
||||
dvd.intro H6)
|
||||
|
||||
theorem lcm_assoc (m n k : ℕ) : lcm (lcm m n) k = lcm m (lcm n k) :=
|
||||
dvd.antisymm
|
||||
(lcm_dvd
|
||||
(lcm_dvd !dvd_lcm_left (dvd.trans !dvd_lcm_left !dvd_lcm_right))
|
||||
(dvd.trans !dvd_lcm_right !dvd_lcm_right))
|
||||
(lcm_dvd
|
||||
(dvd.trans !dvd_lcm_left !dvd_lcm_left)
|
||||
(lcm_dvd (dvd.trans !dvd_lcm_right !dvd_lcm_left) !dvd_lcm_right))
|
||||
|
||||
end nat
|
||||
|
|
|
|||
|
|
@ -401,13 +401,13 @@ strong_induction_on a (
|
|||
theorem by_cases_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y :=
|
||||
cases_on y H0 (take y, H1 !succ_pos)
|
||||
|
||||
theorem zero_or_pos {n : ℕ} : n = 0 ∨ n > 0 :=
|
||||
theorem eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 :=
|
||||
or_of_or_of_imp_left
|
||||
(or.swap (lt_or_eq_of_le !zero_le))
|
||||
(take H : 0 = n, H⁻¹)
|
||||
|
||||
theorem pos_of_ne_zero {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
||||
or.elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
|
||||
or.elim !eq_zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
|
||||
|
||||
theorem ne_zero_of_pos {n : ℕ} (H : n > 0) : n ≠ 0 :=
|
||||
ne.symm (ne_of_lt H)
|
||||
|
|
@ -415,6 +415,12 @@ ne.symm (ne_of_lt H)
|
|||
theorem exists_eq_succ_of_pos {n : ℕ} (H : n > 0) : exists l, n = succ l :=
|
||||
exists_eq_succ_of_lt H
|
||||
|
||||
theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : m | n) (H2 : n > 0) : m > 0 :=
|
||||
pos_of_ne_zero
|
||||
(assume H3 : m = 0,
|
||||
have H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
|
||||
ne_of_lt H2 H4⁻¹)
|
||||
|
||||
/- multiplication -/
|
||||
|
||||
theorem mul_lt_mul_of_le_of_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) :
|
||||
|
|
@ -441,7 +447,7 @@ theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) :
|
|||
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem eq_zero_or_eq_of_mul_eq_mul_left {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k :=
|
||||
or_of_or_of_imp_right zero_or_pos
|
||||
or_of_or_of_imp_right !eq_zero_or_pos
|
||||
(assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H)
|
||||
|
||||
theorem eq_zero_or_eq_of_mul_eq_mul_right {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k :=
|
||||
|
|
|
|||
Loading…
Reference in a new issue