Theorem inv_nonpos

Modification history