In [1]:

```
import proveit
from proveit import defaults
theory = proveit.Theory() # the theorem's theory
```

In [2]:

```
%proving commutation
```

Not quite readily provable because of unusable proofs to avoid circular logic.

In [3]:

```
defaults.assumptions = commutation.conditions
```

In [4]:

```
commutation.instance_expr.conclude_via_mutual_implication()
```

In [5]:

```
%qed
```

Out[5]: