(8steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: div rem properties 1 1 1 1
1. n:
2. 0 = (0 n)n+(0 rem n)
3. 0n
4. 0(0 rem n) & (0 rem n) < n
(0 n) = 0
By:
Decide (1(0 n))
THEN
Decide ((0 n)-1)
THEN
AllHyps (h. Using [`n',n] (FwdThru Thm* a,b:, n:. ab nanb [h]))
Generated subgoals:

None

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequalimpliesandall

(8steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc