Using the following code:

```
n = Int('n')
s = Solver()
s.add(n >= 5)
s.add(Not( n**5 <= 5**n))
print s
print s.check()
```

we obtain the following output:

```
[n ? 5, ¬(n^5 ? 5^n)]
unknown
```

It is to say that Z3Py is not able to produce a direct proof.

Now using the code

```
n = Int('n')
prove(Implies(n >= 5, n**5 <= 5**n))
```

Z3Py also fails.

A posible indirect proof is as follows:

```
n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
prove(Implies(And(e >=0, f >= 0), t >= 0))
```

and the output is:

```
proved
```

A proof using Isabelle + Maple is given at :Theorems and Algorithms: An Interface between Isabelle and Maple. Clemens Ballarin. Karsten Homann. Jacques Calmet.

Other possible indirect proof using Z3Py is as follows:

```
n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
s = Solver()
s.add(e >= 0, f >= 0)
s.add(Not(t >= 0))
print s
print s.check()
```

and the output is:

```
[e ? 0,
f ? 0,
¬(7849 +
9145·f +
4090·f·f +
890·f·f·f +
95·f·f·f·f +
4·f·f·f·f·f +
5·e ?
0)]
unsat
```

Please let me know if it is possible to have a more direct proof using Z3Py. Many thanks.