theorem divid (a: nat): $ a != 0 -> a // a = 1 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | diveq1 | a * 1 = a -> a * 1 // a = a // a |
|
2 | mul12 | a * 1 = a |
|
3 | 1, 2 | ax_mp | a * 1 // a = a // a |
4 | muldiv2 | a != 0 -> a * 1 // a = 1 |
|
5 | 3, 4 | syl5eqr | a != 0 -> a // a = 1 |