Theorem pow_inv_comm₀

Modification history