have : (p + q)/2 < q := calc
  _ ≃ (p + q)/2 := eqv_refl
  _ < (q + q)/2 := lt_substN_div_pos (lt_substL_add ‹p < q›)
  _ ≃ (2 * q)/2 := div_substL (eqv_symm mul_two_add)
  _ ≃ q         := mulL_div_same
ℕ ℤ ℚ : 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
ℕ ℤ ℚ : 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
this : (p + q) / 2 < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q