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

State before:
a b : ℕ
h : b ≠ 0
⊢ gcd_c1 a b = gcd_c2 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_c1 a b = gcd_c2 b (a % b)

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

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