Metamath Proof Explorer

Table of Contents - 15.2.8. Less-than relation in geometric congruences

1. cleg
2. df-leg
3. legval
4. legov
5. legov2
6. legid
7. btwnleg
8. legtrd
9. legtri3
10. legtrid
11. leg0
12. legeq
13. legbtwn
14. tgcgrsub2
15. ltgseg
16. ltgov
17. legov3
18. legso