theorem minle2 (a b: nat): $ min a b <= b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leeq1 | min b a = min a b -> (min b a <= b <-> min a b <= b) |
|
| 2 | mincom | min b a = min a b |
|
| 3 | 1, 2 | ax_mp | min b a <= b <-> min a b <= b |
| 4 | minle1 | min b a <= b |
|
| 5 | 3, 4 | mpbi | min a b <= b |