graph 1 1 Sections Graphs Doc

RankTheoremName
6 Thm* a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n)[div_rem_unique]
cites
1 Thm* 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)[div_rem_properties]
5 Thm* a,b:. |ab| = |a||b|[absval_mul]
0 Thm* a,b:, n:. ab nanb[mul_preserves_le]

graph 1 1 Sections Graphs Doc