auto real_add_int_int

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

auto real_add_int_rat

real_add_int_rat: (all n:Int, r:Rat. real(n) + real(r) = real(rat(n) + r))

auto real_add_rat_int

real_add_rat_int: (all q:Rat, m:Int. real(q) + real(m) = real(q + rat(m)))

auto real_add_rat_rat

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

auto real_div_int_int

real_div_int_int: (all n:Int, m:Int. real(n) / real(m) = real(rat(n) * inv(rat(m))))

auto real_div_int_rat

real_div_int_rat: (all n:Int, r:Rat. real(n) / real(r) = real(rat(n) / r))

auto real_div_rat_int

real_div_rat_int: (all q:Rat, m:Int. real(q) / real(m) = real(q / rat(m)))

auto real_div_rat_rat

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

auto real_eq_int_int

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

auto real_eq_int_rat

real_eq_int_rat: (all n:Int, r:Rat. (real(n) = real(r)) = (rat(n) = r))

auto real_eq_rat_int

real_eq_rat_int: (all q:Rat, m:Int. (real(q) = real(m)) = (q = rat(m)))

auto real_eq_rat_rat

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

auto real_inv_int

real_inv_int: (all n:Int. inv(real(n)) = real(inv(rat(n))))

auto real_inv_rat

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

auto real_le_int_int

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

auto real_le_int_rat

real_le_int_rat: (all n:Int, r:Rat. (real(n) ≤ real(r)) = (rat(n) ≤ r))

auto real_le_rat_int

real_le_rat_int: (all q:Rat, m:Int. (real(q) ≤ real(m)) = (q ≤ rat(m)))

auto real_le_rat_rat

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

auto real_less_int_int

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

auto real_less_int_rat

real_less_int_rat: (all n:Int, r:Rat. (real(n) < real(r)) = (rat(n) < r))

auto real_less_rat_int

real_less_rat_int: (all q:Rat, m:Int. (real(q) < real(m)) = (q < rat(m)))

auto real_less_rat_rat

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

auto real_mult_int_int

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

auto real_mult_int_rat

real_mult_int_rat: (all n:Int, r:Rat. real(n) * real(r) = real(rat(n) * r))

auto real_mult_rat_int

real_mult_rat_int: (all q:Rat, m:Int. real(q) * real(m) = real(q * rat(m)))

auto real_mult_rat_rat

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

auto real_neg_int

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

auto real_neg_rat

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

auto real_rat_int

auto real_sub_int_int

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

auto real_sub_int_rat

real_sub_int_rat: (all n:Int, r:Rat. real(n) - real(r) = real(rat(n) - r))

auto real_sub_rat_int

real_sub_rat_int: (all q:Rat, m:Int. real(q) - real(m) = real(q - rat(m)))

auto real_sub_rat_rat

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