theorem dvdmul2 (a b: nat): $ a || a * b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dvdeq2 | b * a = a * b -> (a || b * a <-> a || a * b) |
|
| 2 | mulcom | b * a = a * b |
|
| 3 | 1, 2 | ax_mp | a || b * a <-> a || a * b |
| 4 | dvdmul1 | a || b * a |
|
| 5 | 3, 4 | mpbi | a || a * b |