-- The Agda standard library
-- Instantiates the natural coefficients ring solver, using coefficient
-- equality induced by ℕ.
-- This is sufficient for proving equalities that are independent of the
-- characteristic.  In particular, this is enough for equalities in
-- rings of characteristic 0.

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra

module Algebra.Solver.Ring.NaturalCoefficients.Default
  {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where

import Algebra.Properties.Semiring.Mult as SemiringMultiplication
open import Data.Maybe.Base using (Maybe; map)
open import Data.Nat using (_≟_)
open import Relation.Binary.Consequences using (dec⇒weaklyDec)
import Relation.Binary.PropositionalEquality.Core as P

open CommutativeSemiring R
open SemiringMultiplication semiring

  dec :  m n  Maybe (m × 1#  n × 1#)
  dec m n = map  { P.refl  refl }) (dec⇒weaklyDec _≟_ m n)

open import Algebra.Solver.Ring.NaturalCoefficients R dec public