{-# OPTIONS --safe #-} module Cubical.Tactics.CommRingSolver.IntAsRawRing where open import Cubical.Data.Nat hiding (_+_; _·_) open import Cubical.Data.Int open import Cubical.Data.Int.Base open import Cubical.Foundations.Prelude open import Cubical.Tactics.CommRingSolver.RawRing ℤAsRawRing : RawRing ℓ-zero ℤAsRawRing = rawring ℤ (pos zero) (pos (suc zero)) _+_ _·_ (λ k → - k) +Ridℤ : (k : ℤ) → (pos zero) + k ≡ k +Ridℤ k = sym (pos0+ k)