calc
  |x * y| = |x| * |y| := by apply abs_mul
  _ ≤ |x| * ε := by apply mul_le_mul; linarith; linarith; apply abs_nonneg; apply abs_nonneg;
  _ < 1 * ε := by rw [mul_lt_mul_right epos]; linarith
  _ = ε := by apply one_mul
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε
no goals