have : p < (p + q)/2 := calc
  _ ≃ p         := eqv_refl
  _ ≃ (2 * p)/2 := eqv_symm mulL_div_same
  _ ≃ (p + p)/2 := div_substL mul_two_add
  _ < (p + q)/2 := lt_substN_div_pos (lt_substR_add ‹p < q›)
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
this : p < (p + q) / 2
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q