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

State before:
n : ℕ
⊢ n ∣ n
Tactic:
apply Exists.intro 1
State after:
n : ℕ
⊢ n = n * 1

State before:
n : ℕ
⊢ n = n * 1
Tactic:
ring
State after:
no goals