kronecker_delta_refl@{} (i : A) : kronecker_delta i i = 1. Proof. unfold kronecker_delta. generalize (dec (i = i)). by rapply decidable_paths_refl. Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.