def ErdosStraus.IsDecomposition (n x y z : Nat) : Prop

A positive triple (x, y, z) is a decomposition for n in the Erdős-Straus equation. We avoid division by using the equivalent natural-number identity 4xyz = n(yz + xz + xy).

Equations

• ErdosStraus.IsDecomposition n x y z = (0 < x ∧ 0 < y ∧ 0 < z ∧ 4 * x * y * z = n * (y * z + x * z + x * y))

def ErdosStraus.HasDecomposition (n : Nat) : Prop

n satisfies the Erdős-Straus property if it has at least one positive decomposition.

Equations

• ErdosStraus.HasDecomposition n = ∃ (x : Nat), ∃ (y : Nat), ∃ (z : Nat), ErdosStraus.IsDecomposition n x y z