Who Cites rem nrel?
rem_nrel	Def Rem(a;n;r) == q:. Div(a;n;q) & qn+r = a
	Thm* a:, n:, r:. Rem(a;n;r) Prop
div_nrel	Def Div(a;n;q) == nq a < n(q+1)
	Thm* a:, n:, q:. Div(a;n;q) Prop
nat	Def == {i:| 0i }
	Thm* Type
nat_plus	Def == {i:| 0 < i }
	Thm* Type
lelt	Def i j < k == ij & j < k
le	Def AB == B < A
	Thm* i,j:. ij Prop
not	Def A == A False
	Thm* A:Prop. (A) Prop

About: