交換律
https://righ1113.hatenablog.com/entry/2020/12/05/074034
Idris
で証明