theorem leadd (a b c d: nat): $ a <= b -> c <= d -> a + c <= b + d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anl | a <= b /\ c <= d -> a <= b |
|
| 2 | anr | a <= b /\ c <= d -> c <= d |
|
| 3 | 1, 2 | leaddd | a <= b /\ c <= d -> a + c <= b + d |
| 4 | 3 | exp | a <= b -> c <= d -> a + c <= b + d |