kronecker_delta_map_inj@{} (i j : A) (f : A -> A) `{!IsInjective f} : kronecker_delta (f i) (f j) = kronecker_delta i j. Proof. unfold kronecker_delta. destruct (dec (i = j)) as [p|p]. - by decidable_true (dec (f i = f j)) (ap f p). - destruct (dec (f i = f j)) as [q|q]. + apply (injective f) in q. contradiction. + reflexivity. Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.