Metamath Proof Explorer

Table of Contents - 5.3.10. Function operation analogue theorems

1. ofsubeq0
2. ofnegsub
3. ofsubge0