Documentation
ErdosStraus
.
SmallCases
Search
return to top
source
Imports
Init
ErdosStraus.Basic
Mathlib.Tactic.IntervalCases
Imported by
ErdosStraus
.
hasDecomposition_two_to_five
source
theorem
ErdosStraus
.
hasDecomposition_two_to_five
{
n
:
ℕ
}
(
hn2
:
2
≤
n
)
(
hn5
:
n
≤
5
)
:
HasDecomposition
n