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

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

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

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