for a, b, c being Element of NAT st (a ^2) + (b ^2) = c ^2 & a,b are_coprime & a is odd holds
ex m, n being Element of NAT st
( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) )