case h
x y b c : ℝ
y✝ : CauSeq ℚ abs
⊢ c + mk y✝ < c + b ↔ mk y✝ < b
x y a b c : ℝ
⊢ c + a < c + b ↔ a < b
induction a using Real.ind_mk
case h.h
x y c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ c + mk y✝¹ < c + mk y✝ ↔ mk y✝¹ < mk y✝
case h
x y b c : ℝ
y✝ : CauSeq ℚ abs
⊢ c + mk y✝ < c + b ↔ mk y✝ < b
induction b using Real.ind_mk
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ + mk y✝² < mk y✝ + mk y✝¹ ↔ mk y✝² < mk y✝¹
case h.h
x y c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ c + mk y✝¹ < c + mk y✝ ↔ mk y✝¹ < mk y✝
induction c using Real.ind_mk
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝ + y✝² < y✝ + y✝¹ ↔ y✝² < y✝¹
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ + mk y✝² < mk y✝ + mk y✝¹ ↔ mk y✝² < mk y✝¹
simp only [mk_lt, ← mk_add]
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ Pos (y✝ + y✝¹ - (y✝ + y✝²)) ↔ Pos (y✝¹ - y✝²)
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝ + y✝² < y✝ + y✝¹ ↔ y✝² < y✝¹
show Pos _ ↔ Pos _
no goals
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ Pos (y✝ + y✝¹ - (y✝ + y✝²)) ↔ Pos (y✝¹ - y✝²)
rw [add_sub_add_left_eq_sub]