Minimum Working Example (MWE)

A minimum working example is a code snippet that can be copied-and-pasted and still have the same features (working) and that does not include unnecessary details (minimum).

Please make sure that your code snippet has:

• correct imports; and
• all the relevant definitions / theorems.

If you post a code snippet on Zulip, please make sure it is surrounded in triple backticks.

```
def my_nat : nat := 5
```