m n : Nat
this : n = n % 0
⊢ gcd 0 n = gcd (n % 0) 0
m n : Nat
⊢ gcd 0 n = gcd (n % 0) 0
have := (mod_zero n).symm
no goals
m n : Nat
this : n = n % 0
⊢ gcd 0 n = gcd (n % 0) 0
rwa [gcd_zero_right]
no goals
m n n✝ : Nat
⊢ gcd (n✝ + 1) n = gcd (n % (n✝ + 1)) (n✝ + 1)
simp [gcd_succ]