rat_den_int: (all n:Int. den(rat(n)) = 1)

rat_frac_div: (all n:Int, d:UInt. frac(n, d) = rat(n) / rat(pos(d)))

rat_int_add: (all n:Int, m:Int. rat(n) + rat(m) = rat(n + m))

rat_int_frac: (all n:Int. rat(n) = frac(n, 1))

rat_int_injective: (all n:Int, m:Int. (if rat(n) = rat(m) then n = m))

rat_int_le: (all n:Int, m:Int. (rat(n) ≤ rat(m)) = (n ≤ m))

rat_int_less: (all n:Int, m:Int. (rat(n) < rat(m)) = (n < m))

rat_int_mult: (all n:Int, m:Int. rat(n) * rat(m) = rat(n * m))

rat_int_neg: (all n:Int. - rat(n) = rat(- n))

rat_int_sub: (all n:Int, m:Int. rat(n) - rat(m) = rat(n - m))

rat_num_int: (all n:Int. num(rat(n)) = n)

rat_uint_int: (all n:UInt. rat(n) = rat(pos(n)))