have p₂: b = b * 2 - b := by 
  rw [Nat.mul_add b 1 1]
  simp
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - (1 + a) < b
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b