Sup of rats

Stream: general

[Johan Commelin]

Do we want some form of supremum for sets of rational numbers? Of course there is always the hassle with the empty set.
What is the cleanest way to state the following problem in Lean:

lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) :
  (1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 :=
begin
end

I want to claim that the 42 is the upper bound and that it is strict.

[Johan Commelin]

For the record, the relevant generalisation to more than 3 nats seems to be discussed in https://www.jstor.org/stable/2299023

[Kevin Buzzard]

Why not just say that if it's less than 1 then it's le 41/42?

[Kevin Buzzard]

The sum of the reciprocals