Theorem add_idem

Modification history