kronecker_delta_symm@{} (i j : A) : kronecker_delta i j = kronecker_delta j i. Proof. unfold kronecker_delta. destruct (dec (i = j)) as [p|q]. - by decidable_true (dec (j = i)) p^. - by decidable_false (dec (j = i)) (symmetric_neq q). Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.