auto rat_frac_lit_add
rat_frac_lit_add: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) + frac(m, fromNat(lit(suc(z)))) = frac(n * pos(fromNat(lit(suc(z)))) + m * pos(fromNat(lit(suc(y)))), fromNat(lit(suc(y))) * fromNat(lit(suc(z)))))
auto rat_frac_lit_add_int
rat_frac_lit_add_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) + rat(m) = frac(n + m * pos(fromNat(lit(suc(y)))), fromNat(lit(suc(y))) * 1))
auto rat_frac_lit_div
rat_frac_lit_div: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) / frac(m, fromNat(lit(suc(z)))) = frac(n, fromNat(lit(suc(y)))) * inv(frac(m, fromNat(lit(suc(z))))))
auto rat_frac_lit_div_int
rat_frac_lit_div_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) / rat(m) = frac(n, fromNat(lit(suc(y)))) * inv(rat(m)))
auto rat_frac_lit_eq
rat_frac_lit_eq: (all n:Int, y:Nat, m:Int, z:Nat. (frac(n, fromNat(lit(suc(y)))) = frac(m, fromNat(lit(suc(z))))) = (n * pos(fromNat(lit(suc(z)))) = m * pos(fromNat(lit(suc(y))))))
auto rat_frac_lit_eq_int
rat_frac_lit_eq_int: (all n:Int, y:Nat, m:Int. (frac(n, fromNat(lit(suc(y)))) = rat(m)) = (n = m * pos(fromNat(lit(suc(y))))))
auto rat_frac_lit_le
rat_frac_lit_le: (all n:Int, y:Nat, m:Int, z:Nat. (frac(n, fromNat(lit(suc(y)))) ≤ frac(m, fromNat(lit(suc(z))))) = (n * pos(fromNat(lit(suc(z)))) ≤ m * pos(fromNat(lit(suc(y))))))
auto rat_frac_lit_le_int
rat_frac_lit_le_int: (all n:Int, y:Nat, m:Int. (frac(n, fromNat(lit(suc(y)))) ≤ rat(m)) = (n ≤ m * pos(fromNat(lit(suc(y))))))
auto rat_frac_lit_less
rat_frac_lit_less: (all n:Int, y:Nat, m:Int, z:Nat. (frac(n, fromNat(lit(suc(y)))) < frac(m, fromNat(lit(suc(z))))) = (n * pos(fromNat(lit(suc(z)))) < m * pos(fromNat(lit(suc(y))))))
auto rat_frac_lit_less_int
rat_frac_lit_less_int: (all n:Int, y:Nat, m:Int. (frac(n, fromNat(lit(suc(y)))) < rat(m)) = (n < m * pos(fromNat(lit(suc(y))))))
auto rat_frac_lit_mult
rat_frac_lit_mult: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) * frac(m, fromNat(lit(suc(z)))) = frac(n * m, fromNat(lit(suc(y))) * fromNat(lit(suc(z)))))
auto rat_frac_lit_mult_int
rat_frac_lit_mult_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) * rat(m) = frac(n * m, fromNat(lit(suc(y))) * 1))
auto rat_frac_lit_neg
rat_frac_lit_neg: (all n:Int, y:Nat. - frac(n, fromNat(lit(suc(y)))) = frac(- n, fromNat(lit(suc(y)))))
auto rat_frac_lit_one
rat_frac_lit_one: (all n:Int. frac(n, 1) = rat(n))
auto rat_frac_lit_reduce
rat_frac_lit_reduce: (all x:Nat, y:Nat. (if 1 < gcd(fromNat(lit(suc(x))), fromNat(lit(suc(y)))) then frac(pos(fromNat(lit(suc(x)))), fromNat(lit(suc(y)))) = frac(pos(fromNat(lit(suc(x)) / gcd(lit(suc(x)), lit(suc(y))))), fromNat(lit(suc(y)) / gcd(lit(suc(x)), lit(suc(y)))))))
auto rat_frac_lit_reduce_neg
rat_frac_lit_reduce_neg: (all x:Nat, y:Nat. (if 1 < gcd(fromNat(lit(suc(x))), fromNat(lit(suc(y)))) then frac(negsuc(fromNat(lit(x))), fromNat(lit(suc(y)))) = frac(- pos(fromNat(lit(suc(x)) / gcd(lit(suc(x)), lit(suc(y))))), fromNat(lit(suc(y)) / gcd(lit(suc(x)), lit(suc(y)))))))
auto rat_frac_lit_sub
rat_frac_lit_sub: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) - frac(m, fromNat(lit(suc(z)))) = frac(n, fromNat(lit(suc(y)))) + frac(- m, fromNat(lit(suc(z)))))
auto rat_frac_lit_sub_int
rat_frac_lit_sub_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) - rat(m) = frac(n, fromNat(lit(suc(y)))) + rat(- m))
auto rat_frac_lit_zero
rat_frac_lit_zero: (all n:Int. frac(n, 0) = rat(+0))
auto rat_frac_zero
auto rat_int_add
auto rat_int_add_frac_lit
rat_int_add_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) + frac(n, fromNat(lit(suc(y)))) = frac(m * pos(fromNat(lit(suc(y)))) + n, 1 * fromNat(lit(suc(y)))))
auto rat_int_div
rat_int_div: (all n:Int, m:Int. rat(n) / rat(m) = rat(n) * inv(rat(m)))
auto rat_int_div_frac_lit
rat_int_div_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) / frac(n, fromNat(lit(suc(y)))) = rat(m) * inv(frac(n, fromNat(lit(suc(y))))))
auto rat_int_eq
rat_int_eq: (all n:Int, m:Int. (rat(n) = rat(m)) = (n = m))
auto rat_int_eq_frac_lit
rat_int_eq_frac_lit: (all m:Int, n:Int, y:Nat. (rat(m) = frac(n, fromNat(lit(suc(y))))) = (m * pos(fromNat(lit(suc(y)))) = n))
auto rat_int_le
auto rat_int_le_frac_lit
rat_int_le_frac_lit: (all m:Int, n:Int, y:Nat. (rat(m) ≤ frac(n, fromNat(lit(suc(y))))) = (m * pos(fromNat(lit(suc(y)))) ≤ n))
auto rat_int_less
auto rat_int_less_frac_lit
rat_int_less_frac_lit: (all m:Int, n:Int, y:Nat. (rat(m) < frac(n, fromNat(lit(suc(y))))) = (m * pos(fromNat(lit(suc(y)))) < n))
auto rat_int_mult
auto rat_int_mult_frac_lit
rat_int_mult_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) * frac(n, fromNat(lit(suc(y)))) = frac(m * n, 1 * fromNat(lit(suc(y)))))
auto rat_int_neg
auto rat_int_sub
auto rat_int_sub_frac_lit
rat_int_sub_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) - frac(n, fromNat(lit(suc(y)))) = rat(m) + frac(- n, fromNat(lit(suc(y)))))
auto rat_inv_frac_lit_neg
rat_inv_frac_lit_neg: (all x:Nat, y:Nat. inv(frac(negsuc(fromNat(lit(x))), fromNat(lit(suc(y))))) = frac(- pos(fromNat(lit(suc(y)))), fromNat(lit(suc(x)))))
auto rat_inv_frac_lit_pos
rat_inv_frac_lit_pos: (all x:Nat, y:Nat. inv(frac(pos(fromNat(lit(suc(x)))), fromNat(lit(suc(y))))) = frac(pos(fromNat(lit(suc(y)))), fromNat(lit(suc(x)))))
auto rat_inv_int_lit_neg
rat_inv_int_lit_neg: (all x:Nat. inv(rat(negsuc(fromNat(lit(x))))) = frac(- 1, fromNat(lit(suc(x)))))
auto rat_inv_int_lit_pos
rat_inv_int_lit_pos: (all x:Nat. inv(rat(pos(fromNat(lit(suc(x)))))) = frac(+1, fromNat(lit(suc(x)))))