theorem leaddsub2i (a b c: nat): $ a + b <= c -> b <= c - a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leeq1 | a + b = b + a -> (a + b <= c <-> b + a <= c) |
|
| 2 | addcom | a + b = b + a |
|
| 3 | 1, 2 | ax_mp | a + b <= c <-> b + a <= c |
| 4 | leaddsubi | b + a <= c -> b <= c - a |
|
| 5 | 3, 4 | sylbi | a + b <= c -> b <= c - a |