40 lines
1.3 KiB
Text
40 lines
1.3 KiB
Text
import data.nat
|
||
open nat eq.ops algebra
|
||
|
||
theorem lcm_dvd {m n k : nat} (H1 : m ∣ k) (H2 : (n ∣ k)) : (lcm m n ∣ k) :=
|
||
match eq_zero_or_pos k with
|
||
| @or.inl _ _ kzero :=
|
||
begin
|
||
rewrite kzero,
|
||
apply dvd_zero
|
||
end
|
||
| @or.inr _ _ kpos :=
|
||
obtain (p : nat) (km : k = m * p), from exists_eq_mul_right_of_dvd H1,
|
||
obtain (q : nat) (kn : k = n * q), from exists_eq_mul_right_of_dvd H2,
|
||
begin
|
||
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 n mpos,
|
||
have ppos : p > 0,
|
||
begin
|
||
apply pos_of_mul_pos_left,
|
||
apply (eq.rec_on km),
|
||
exact kpos
|
||
end,
|
||
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),
|
||
begin
|
||
apply sorry
|
||
end,
|
||
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,
|
||
begin
|
||
rewrite [-mul.assoc, gcd_mul_lcm],
|
||
exact H4
|
||
end,
|
||
have H6 : lcm m n * gcd p q = k, from
|
||
!eq_of_mul_eq_mul_left gcd_pos H5,
|
||
exact (dvd.intro H6)
|
||
end
|
||
end
|