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

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