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

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