# Frobenius Number in Two Variables #

In this file we first define a predicate for Frobenius numbers, then solve the 2-variable variant of this problem.

## Theorem Statement #

Given a finite set of relatively prime integers all greater than 1, their Frobenius number is the
largest positive integer that cannot be expressed as a sum of nonnegative multiples of these
integers. Here we show the Frobenius number of two relatively prime integers `m`

and `n`

greater
than 1 is `m * n - m - n`

. This result is also known as the Chicken McNugget Theorem.

## Implementation Notes #

First we define Frobenius numbers in general using `IsGreatest`

and `AddSubmonoid.closure`

. Then
we proceed to compute the Frobenius number of `m`

and `n`

.

For the upper bound, we begin with an auxiliary lemma showing `m * n`

is not attainable, then show
`m * n - m - n`

is not attainable. Then for the construction, we create a `k_1`

which is `k mod n`

and `0 mod m`

, then show it is at most `k`

. Then `k_1`

is a multiple of `m`

, so `(k-k_1)`

is a multiple of n, and we're done.

## Tags #

frobenius number, chicken mcnugget, chinese remainder theorem, add_submonoid.closure

A natural number `n`

is the **Frobenius number** of a set of natural numbers `s`

if it is an
upper bound on the complement of the additive submonoid generated by `s`

.
In other words, it is the largest number that can not be expressed as a sum of numbers in `s`

.

## Equations

- FrobeniusNumber n s = IsGreatest { k | ¬k ∈ AddSubmonoid.closure s } n

The **Chicken Mcnugget theorem** stating that the Frobenius number
of positive numbers `m`

and `n`

is `m * n - m - n`

.