theorem ltsubadd (a b c: nat): $ b <= a -> (a - b < c <-> a < c + b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltadd1 | a - b < c <-> a - b + b < c + b |
|
| 2 | npcan | b <= a -> a - b + b = a |
|
| 3 | 2 | lteq1d | b <= a -> (a - b + b < c + b <-> a < c + b) |
| 4 | 1, 3 | syl5bb | b <= a -> (a - b < c <-> a < c + b) |