Thm* a: , n: . (a mod n)  | [modulus_wf] |
Thm* a: , n: . ((a rem n) rem n) = (a rem n) | [rem_rem_to_rem] |
Thm* i,j: , n: . (((i rem n)+(j rem n)) rem n) = ((i+j) rem n) | [rem_addition] |
Thm* a,b: , n: . ((a+b n) rem n) = (a rem n) | [rem_invariant] |
Thm* a: , n: . a n  (a rem n) = ((a-n) rem n) | [rem_rec_case] |
Thm* a: , n: . a<n  (a rem n) = a | [rem_base_case] |
Thm* a: , n: . a n  (a n) = ((a-n) n)+1 | [div_rec_case] |
Thm* a: , n: . a<n  (a n) = 0 | [div_base_case] |
Thm* a: , n: . Rem(a;n;a rem n) | [rem_fun_sat_rem_nrel] |
Thm* a: , n: , k: . k (a n)  k n a | [div_lbound_1] |
Thm* a: , n: , p,q: . Div(a;n;p)  Div(a;n;q)  p = q | [div_unique] |
Thm* a: , n: . q: . Div(a;n;q) & (a n) = q | [div_elim] |
Thm* a: , n: . Div(a;n;a n) | [div_fun_sat_div_nrel] |
Thm* a: , n: . 0 (a n) | [div_bounds_1] |
Thm* a: , n:{...-1}. (a rem n) = (a rem -n) | [rem_4_to_1] |
Thm* a: , n:{...-1}. (a n) {...0} | [division_typing2b_sfa] |
Thm* a:{...0}, n:{...-1}. (a n)  | [division_typing2a_sfa] |
Thm* a: , n: . (a n)  | [division_typing1a_sfa] |
Thm* a: , b:{...-1}. (a b) = -(a (-b)) | [div_4_to_1] |
Thm* a: , n:{...-1}. (a rem n) (-n) | [rem_bounds_4_typing_sfa] |
Thm* a: , n: . (a rem n) n | [rem_bounds_1_typing_sfa] |
Thm* a: , n:{...-1}. 0 (a rem n) & (a rem n)<-n | [rem_bounds_4] |
Thm* a: , n: . 0 (a rem n) & (a rem n)<n | [rem_bounds_1] |
Thm* a,b: . (a -- (a -- b)) = imin(a;b) | [ndiff_ndiff_eq_imin] |
Thm* a,b: , c: . ((a -- b) -- c) = (a -- (b+c)) | [ndiff_ndiff] |
Thm* a: , b: . ((a+b) -- b) = a | [ndiff_inv] |
Thm* a: . (0 -- a) = 0 | [ndiff_ann_l] |
Thm* a: . (a -- 0) = a | [ndiff_id_r] |
Thm* P:(  Prop). ( x: . P(|x|))  ( x: . P(x)) | [absval_elim] |
Thm* i: , n: . |i|>n  i<-n i>n | [absval_lbound] |
Thm* i: , n: . |i| n  -n i & i n | [absval_ubound] |
Thm* i: . |i| = i | [absval_pos] |
Thm* x: . |x|  | [absval_wf] |
Thm* i,j: . i j  | [multiply_nat_wf] |
Thm* a,b: . 0 a b | [mul_bounds_1a] |
Thm* i1,i2,j1,j2: . i1 j1  i2 j2  i1 i2 j1 j2 | [multiply_functionality_wrt_le] |
Thm* a,b: , n: . a b  n a n b | [mul_preserves_le] |
Def Rem(a;n;r) == q: . Div(a;n;q) & q n+r = a | [rem_nrel] |