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 |