rat_add_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then frac(n, d) + frac(m, e) = frac(n * pos(e) + m * pos(d), d * e)))

rat_den_pos: (all x:Rat. 0 < den(x))

rat_frac_cross: (all n:Int, d:UInt. (if 0 < d then num(frac(n, d)) * pos(d) = n * pos(den(frac(n, d)))))

rat_frac_cross_eq: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e) and (n * pos(e) = m * pos(d))) then frac(n, d) = frac(m, e)))

rat_frac_eq_cross: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e) and (frac(n, d) = frac(m, e))) then n * pos(e) = m * pos(d)))

rat_frac_eq_iff: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then (frac(n, d) = frac(m, e)) = (n * pos(e) = m * pos(d))))

rat_frac_neg: (all n:Int, d:UInt. frac(- n, d) = - frac(n, d))

rat_frac_num_den: (all x:Rat. frac(num(x), den(x)) = x)

rat_frac_rep: (all x:Rat. some n:Int,d:UInt. ((0 < d) and (x = frac(n, d))))

rat_frac_scale: (all k:UInt, n:Int, d:UInt. (if 0 < k then frac(pos(k) * n, k * d) = frac(n, d)))

rat_le_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then (frac(n, d) ≤ frac(m, e)) = (n * pos(e) ≤ m * pos(d))))

rat_less_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then (frac(n, d) < frac(m, e)) = (n * pos(e) < m * pos(d))))

rat_mult_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then frac(n, d) * frac(m, e) = frac(n * m, d * e)))