rat_add_assoc: (all x:Rat, y:Rat, z:Rat. (x + y) + z = x + (y + z))

rat_add_both_sides_of_equal: (all x:Rat, y:Rat, z:Rat. (x + y = x + z) = (y = z))

rat_add_both_sides_of_equal_right: (all x:Rat, y:Rat, z:Rat. (y + x = z + x) = (y = z))

rat_add_commute: (all x:Rat, y:Rat. x + y = y + x)

rat_add_inverse: (all x:Rat. x + - x = rat(+0))

rat_add_left_inverse: (all x:Rat. - x + x = rat(+0))

rat_add_sub_cancel: (all x:Rat, y:Rat. (x + y) - y = x)

auto rat_add_zero

rat_add_zero: (all x:Rat. x + rat(+0) = x)

rat_frac_zero: (all d:UInt. frac(+0, d) = rat(+0))

rat_neg_distr_add: (all x:Rat, y:Rat. - (x + y) = - x + - y)

rat_neg_injective: (all x:Rat, y:Rat. (if - x = - y then x = y))

rat_neg_involutive: (all x:Rat. - (- x) = x)

rat_neg_sub: (all x:Rat, y:Rat. - (x - y) = y - x)

auto rat_neg_zero

rat_neg_zero: - rat(+0) = rat(+0)

rat_sub_add_cancel: (all x:Rat, y:Rat. (x - y) + y = x)

auto rat_sub_cancel

rat_sub_cancel: (all x:Rat. x - x = rat(+0))

rat_sub_def: (all x:Rat, y:Rat. x - y = x + - y)

rat_sub_eq_zero_iff: (all x:Rat, y:Rat. (x - y = rat(+0)) = (x = y))

auto rat_sub_zero

rat_sub_zero: (all x:Rat. x - rat(+0) = x)

auto rat_zero_add

rat_zero_add: (all x:Rat. rat(+0) + x = x)

auto rat_zero_sub

rat_zero_sub: (all x:Rat. rat(+0) - x = - x)