Theorem: HTPI.gcd_c2_nonzero (HTPILib/Chap7.lean)

State before:
a b : ℕ
h : b ≠ 0
⊢ gcd_c2 a b = gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)
Tactic:
obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h
State after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a b = gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)

State before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a b = gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)
Tactic:
rewrite [h2]
State after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a (n + 1) = gcd_c1 (n + 1) (a % (n + 1)) - gcd_c2 (n + 1) (a % (n + 1)) * ↑(a / (n + 1))

State before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a (n + 1) = gcd_c1 (n + 1) (a % (n + 1)) - gcd_c2 (n + 1) (a % (n + 1)) * ↑(a / (n + 1))
Tactic:
rfl
State after:
no goals