[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ ↑(natAbs ((fun x x_1 => x % x_1) a b)) < ↑(natAbs b)
[PROOFSTEP]
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ a % b < |b|
[PROOFSTEP]
exact Int.emod_lt _ b0
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ natAbs (a * b) ≥ natAbs a
[PROOFSTEP]
rw [← mul_one a.natAbs, Int.natAbs_mul]
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ natAbs a * natAbs b ≥ natAbs a * 1
[PROOFSTEP]
rw [← Int.natAbs_pos] at b0 
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : 0 < natAbs b
⊢ natAbs a * natAbs b ≥ natAbs a * 1
[PROOFSTEP]
exact Nat.mul_le_mul_of_nonneg_left b0
[GOAL]
K : Type u_1
inst✝ : Field K
a b : K
⊢ b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
[PROOFSTEP]
by_cases h : b = 0
[GOAL]
case pos
K : Type u_1
inst✝ : Field K
a b : K
h : b = 0
⊢ b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
[PROOFSTEP]
simp [h, mul_div_cancel']
[GOAL]
case neg
K : Type u_1
inst✝ : Field K
a b : K
h : ¬b = 0
⊢ b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
[PROOFSTEP]
simp [h, mul_div_cancel']
[GOAL]
K : Type u_1
inst✝ : Field K
a b : K
hnb : b ≠ 0
⊢ (fun a b => a = 0 ∧ b ≠ 0) ((fun a b => a - a * b / b) a b) b
[PROOFSTEP]
simp [hnb]
