kronecker_delta_neq@{} {i j : A} (p : i <> j) : kronecker_delta i j = 0. Proof. unfold kronecker_delta. by decidable_false (dec (i = j)) p. Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.