theorem idvd (a b c: nat): $ c * a = b -> a || b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | muleq1 | x = c -> x * a = c * a |
|
| 2 | 1 | eqeq1d | x = c -> (x * a = b <-> c * a = b) |
| 3 | 2 | iexe | c * a = b -> E. x x * a = b |
| 4 | 3 | conv dvd | c * a = b -> a || b |