diff --git a/RealClosedField/RealClosedField/FormallyReal.lean b/RealClosedField/RealClosedField/FormallyReal.lean
index 2ff844f..34b6409 100644
--- a/RealClosedField/RealClosedField/FormallyReal.lean
+++ b/RealClosedField/RealClosedField/FormallyReal.lean
@@ -35,7 +35,7 @@ theorem isFormallyReal_of_eq_zero_of_mul_self_of_eq_zero_of_add
 
 instance IsFormallyReal.instIsSemireal [NonAssocSemiring R] [Nontrivial R] [IsFormallyReal R] :
     IsSemireal R where
-  add_one_ne_zero_of_isSumSq hs h_contr := by
+  one_add_ne_zero hs h_contr := by
     simpa using IsFormallyReal.eq_zero_of_add_left (by aesop) hs h_contr
 
 instance LinearOrderedRing.instIsFormallyReal [LinearOrderedRing R] : IsFormallyReal R where
diff --git a/RealClosedField/RealClosedField/Semireal/Field.lean b/RealClosedField/RealClosedField/Semireal/Field.lean
index 1ccf701..d58554a 100644
--- a/RealClosedField/RealClosedField/Semireal/Field.lean
+++ b/RealClosedField/RealClosedField/Semireal/Field.lean
@@ -22,7 +22,7 @@ instance (O : RingPreordering F) [RingPreordering.IsOrdering O] : IsMaxCone O wh
 instance IsSemireal.instIsFormallyReal [IsSemireal F] : IsFormallyReal F where
   eq_zero_of_mul_self_add {a} {s} hs h := by
     by_contra
-    exact add_one_ne_zero_of_isSumSq (by aesop) (show 1 + s * (a⁻¹ * a⁻¹) = 0 by field_simp [h])
+    exact one_add_ne_zero (by aesop) (show 1 + s * (a⁻¹ * a⁻¹) = 0 by field_simp [h])
 
 variable [IsSemireal F]