real_frac: (all n:Int, d:UInt. (if 0 < d then real(frac(n, d)) = real(n) * inv(real(d))))

real_int_add: (all n:Int, m:Int. real(n + m) = real(n) + real(m))

real_int_eq: (all n:Int, m:Int. (real(n) = real(m)) = (n = m))

real_int_injective: (all n:Int, m:Int. (if real(n) = real(m) then n = m))

real_int_le: (all n:Int, m:Int. (real(n) ≤ real(m)) = (n ≤ m))

real_int_less: (all n:Int, m:Int. (real(n) < real(m)) = (n < m))

real_int_mult: (all n:Int, m:Int. real(n * m) = real(n) * real(m))

real_int_neg: (all n:Int. real(- n) = - real(n))

real_int_negsuc: (all a:UInt. real(negsuc(a)) = - real(1 + a))

real_int_nonneg_iff: (all n:Int. (real(+0) ≤ real(n)) = (+0 ≤ n))

real_int_pos: (all a:UInt. real(pos(a)) = real(a))

real_int_sub: (all n:Int, m:Int. real(n - m) = real(n) - real(m))

real_rat_add: (all q:Rat, r:Rat. real(q + r) = real(q) + real(r))

real_rat_def: (all q:Rat. real(q) = real(num(q)) * inv(real(den(q))))

real_rat_div: (all q:Rat, r:Rat. real(q / r) = real(q) / real(r))

real_rat_eq: (all q:Rat, r:Rat. (real(q) = real(r)) = (q = r))

real_rat_int: (all n:Int. real(rat(n)) = real(n))

real_rat_inv: (all q:Rat. real(inv(q)) = inv(real(q)))

real_rat_le: (all q:Rat, r:Rat. (real(q) ≤ real(r)) = (q ≤ r))

real_rat_less: (all q:Rat, r:Rat. (real(q) < real(r)) = (q < r))

real_rat_mult: (all q:Rat, r:Rat. real(q * r) = real(q) * real(r))

real_rat_neg: (all q:Rat. real(- q) = - real(q))

real_rat_sub: (all q:Rat, r:Rat. real(q - r) = real(q) - real(r))

real_uint_add: (all m:UInt, n:UInt. real(m + n) = real(m) + real(n))

real_uint_injective: (all m:UInt, n:UInt. (if real(m) = real(n) then m = n))

real_uint_le: (all m:UInt, n:UInt. (if m ≤ n then real(m) ≤ real(n)))

real_uint_le_iff: (all m:UInt, n:UInt. (real(m) ≤ real(n)) = (m ≤ n))

real_uint_less: (all m:UInt, n:UInt. (if m < n then real(m) < real(n)))

real_uint_mult: (all m:UInt, n:UInt. real(m * n) = real(m) * real(n))

real_uint_nonneg: (all n:UInt. real(+0) ≤ real(n))

real_uint_pos: (all n:UInt. (if 0 < n then real(+0) < real(n)))

real_uint_suc: (all n:UInt. real(1 + n) = real(+1) + real(n))