{R : Ring} {i j : nat} (p : (i < j)%nat) : kronecker_delta (R:=R) i j = 0. Proof. apply kronecker_delta_neq. intros q; destruct q. by apply lt_irrefl in p. Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.