prob10:theory begin
for_a:lemma forall(a:posreal,b:posreal,c:int,m:int,n:int):1 / a + 1 / b = 1 =>
c <= m * a & m * a < c + 1 => c <= n * b & n * b < c + 1 => c = m * a
%|- for_a : PROOF
%|- (then (skeep)
%|- (spread (case "c < m * a")
%|- ((spread (case "c/a <m & m<(c+1)/a & c/b<=n & n<(c+1)/b")
%|- ((then (delete -2 -4 -5 -6 -7) (flatten)
%|- (spread (case "c*(1/a+1/b)<m+n & m+n<(c+1)*(1/a+1/b)")
%|- ((then (replace -6 * LR) (grind-reals)) (grind-reals))))
%|- (grind-reals)))
%|- (ground))))
%|- QED
for_a_b:lemma forall(a:posreal,b:posreal,c:int,m:int,n:int):1 / a + 1 / b = 1 =>
c <= m * a & m * a < c + 1 => c <= n * b & n * b < c + 1 => c = m * a & c = n * b
%|- for_a_b : PROOF
%|- (then (skeep) (lemma "for_a")
%|- (spread (split 1)
%|- ((then (inst -1 "a" "b" "c" "m" "n") (grind))
%|- (then (inst -1 "b" "a" "c" "n" "m") (grind)))))
%|- QED
prob10:theorem forall (a: posreal, b: posreal, m: int, n: int):
1 / a + 1 / b = 1 =>
not (exists (p: rat): a = p) & not (exists (q: rat): b = q) =>
(m /= 0 or n /= 0) => floor(m * a) /= floor(n * b)
%|- prob10 : PROOF
%|- (then (skeep) (lemma "floor_def" ("x" "m * a"))
%|- (lemma "floor_def" ("x" "n * b")) (name "c" "floor(n*b)")
%|- (replace -1 * LR) (replace -6 * LR) (lemma "for_a_b")
%|- (inst -1 "a" "b" "c" "m" "n")
%|- (spread (split -6)
%|- ((then (inst 1 "c/m") (grind-reals))
%|- (then (inst 2 "c/n") (grind-reals)))))
%|- QED
end prob10
