Theorem Equiv.piCongrLeft_sum_inr

Modification history