diff --git a/analysis/Analysis/Section_4_2.lean b/analysis/Analysis/Section_4_2.lean
index 66b49073..a86647fe 100644
--- a/analysis/Analysis/Section_4_2.lean
+++ b/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