theorem lemax2 (a b: nat): $ b <= max a b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leeq2 | max b a = max a b -> (b <= max b a <-> b <= max a b) |
|
| 2 | maxcom | max b a = max a b |
|
| 3 | 1, 2 | ax_mp | b <= max b a <-> b <= max a b |
| 4 | lemax1 | b <= max b a |
|
| 5 | 3, 4 | mpbi | b <= max a b |