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

State before:
a : ℕ
⊢ gcd a 0 = a
Tactic:
rfl
State after:
no goals