theorem dfle (a b: nat) {x: nat}: $ a <= b <-> E. x a + x = b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | addeq2 | y = x -> a + y = a + x |
|
| 2 | 1 | eqeq1d | y = x -> (a + y = b <-> a + x = b) |
| 3 | 2 | cbvex | E. y a + y = b <-> E. x a + x = b |
| 4 | 3 | conv le | a <= b <-> E. x a + x = b |