kronecker_delta@{} (i j : A) : R := if dec (i = j) then 1 else 0.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.