a b : Int
Ha : 0 ≤ a
this : a / b ≤ ↑(natAbs a)
⊢ a / b ≤ a
a b : Int
Ha : 0 ≤ a
⊢ a / b ≤ a
have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_div_le_natAbs a b)
no goals
a b : Int
Ha : 0 ≤ a
this : a / b ≤ ↑(natAbs a)
⊢ a / b ≤ a
rwa [natAbs_of_nonneg Ha] at this