Merge pull request #429 from brandondong/rat_sub

Add missing 4.2 definition

Author: teorth

analysis/Analysis/Section_4_2.lean

@@ -237,6 +237,9 @@ instance Rat.instField : Field Rat where
 
 example : (3//4) / (5//6) = 9 // 10 := by sorry
 
+/-- Definition of subtraction -/
+theorem Rat.sub_eq (a b:Rat) : a - b = a + (-b) := by rfl
+
 def Rat.coe_int_hom : ℤ →+* Rat where
   toFun n := (n:Rat)
   map_zero' := rfl