f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (Int.toNat (↑f 0).num)) / ↑↑(Nat.sqrt (↑f 0).den)
f : CauSeq ℚ abs
⊢ 0 ≤ sqrtAux f 0
rw [sqrtAux, Rat.mkRat_eq, Rat.divInt_eq_div]
no goals
f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (Int.toNat (↑f 0).num)) / ↑↑(Nat.sqrt (↑f 0).den)
apply div_nonneg <;>
exact Int.cast_nonneg.2 (Int.ofNat_nonneg _)