case h
x y b : ℝ
a : CauSeq ℚ abs
⊢ 0 < mk a → 0 < b → 0 < mk a * b
x y a b : ℝ
⊢ 0 < a → 0 < b → 0 < a * b
induction' a using Real.ind_mk with a
case h.h
x y : ℝ
a b : CauSeq ℚ abs
⊢ 0 < mk a → 0 < mk b → 0 < mk a * mk b
case h
x y b : ℝ
a : CauSeq ℚ abs
⊢ 0 < mk a → 0 < b → 0 < mk a * b
induction' b using Real.ind_mk with b
no goals
case h.h
x y : ℝ
a b : CauSeq ℚ abs
⊢ 0 < mk a → 0 < mk b → 0 < mk a * mk b
simpa only [mk_lt, mk_pos, ← mk_mul] using CauSeq.mul_pos