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

At: div rem properties
a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)
By:
RepeatFor 2 (Analyze 0)
THEN
Inst Thm* a:, n:. a = (a n)n+(a rem n) [a;n]
THEN
Assert (|a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0))
Generated subgoals:

11. a:
2. n:
3. a = (a n)n+(a rem n)
|a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)		6 steps
 
21. a:
2. n:
3. a = (a n)n+(a rem n)
4. |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)
a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)		1 step

About:
intnatural_numberaddmultiplydivideremainderless_thanequalimpliesandall

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