Theorem pigeonhole
    :  forall m n : nat, m < n
    -> forall f : nat -> nat, (forall i, f i < m)
    -> exists i, i < n
    -> exists j, j < i / f i = f j.