a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div ↑w✝¹ ↑w✝) = Nat.div (natAbs ↑w✝¹) (natAbs ↑w✝)
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div (↑w✝¹) (-↑w✝)) = Nat.div (natAbs ↑w✝¹) (natAbs (-↑w✝))
rw [Int.div_neg, natAbs_neg, natAbs_neg]
no goals
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div ↑w✝¹ ↑w✝) = Nat.div (natAbs ↑w✝¹) (natAbs ↑w✝)
rfl
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div ↑w✝¹ ↑w✝) = Nat.div (natAbs ↑w✝¹) (natAbs ↑w✝)
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div (-↑w✝¹) ↑w✝) = Nat.div (natAbs (-↑w✝¹)) (natAbs ↑w✝)
rw [Int.neg_div, natAbs_neg, natAbs_neg]
no goals
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div ↑w✝¹ ↑w✝) = Nat.div (natAbs ↑w✝¹) (natAbs ↑w✝)
rfl
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div ↑w✝¹ ↑w✝) = Nat.div (natAbs ↑w✝¹) (natAbs ↑w✝)
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div (-↑w✝¹) (-↑w✝)) = Nat.div (natAbs (-↑w✝¹)) (natAbs (-↑w✝))
rw [Int.neg_div_neg, natAbs_neg, natAbs_neg]
no goals
a b : Int
w✝¹ w✝ : Nat
⊢ natAbs (div ↑w✝¹ ↑w✝) = Nat.div (natAbs ↑w✝¹) (natAbs ↑w✝)
rfl