theorem leaddid1 (a b: nat): $ a <= a + b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | addeq2 | x = b -> a + x = a + b |
|
| 2 | 1 | eqeq1d | x = b -> (a + x = a + b <-> a + b = a + b) |
| 3 | 2 | iexe | a + b = a + b -> E. x a + x = a + b |
| 4 | 3 | conv le | a + b = a + b -> a <= a + b |
| 5 | eqid | a + b = a + b |
|
| 6 | 4, 5 | ax_mp | a <= a + b |